source: sizechecking_branches/SE.hs @ 29

{-# Language GADTs,
        FlexibleInstances,
        FlexibleContexts,
        ScopedTypeVariables,
        TypeFamilies,
        NoMonomorphismRestriction,
        OverlappingInstances #-}

module SE where

import LL

class SizeExp l where
    type List l :: * -> *
    list    :: l Int -> l (Arr l Int b) -> l (List l b)
    aabs    :: (l Int -> l (Arr l Int a) -> l b) -> l (Arr l (List l a) b)
    shift   :: l (Arr l Int a) -> l Int -> l (Arr l Int a) -> l (Arr l Int a)
    undef   :: l Bottom
    unsized :: l ()


instance SizeExp R where
  type List R = RList
  undef       = R $ Bottom
  unsized     = R $ ()
  list s f    = R $ RList (unR s, unR . (unR f) . R )
  aabs e = R $ ( \(RList (s,f)) -> (e (R s) (R (R . f . unR))) ) . unR
  shift a s c = R $ \i -> if (unR i)<(unR s) then unR a i else unR c i

x = aabs (\s _ -> s) `app` list (lit 0) (labs $ \_ -> undef)
--y = list 0 $ labs $ \_ -> undef
--conss = labs $ \x -> aabs $ \ys yf -> list (ys + 1) $ shift yf ys (labs $ \_ -> x)
--concats = aabs $ \xs xf -> (aabs $ \ys yf -> list (xs+ys) $ shift xf xs yf)
--maps = labs $ \x -> aabs $ \ys yf -> list ys ( x `app` yf )
--l0 = list (lit 0) (labs $ \_ -> unsized)
--l1 = list (lit 1) (labs $ \_ -> unsized)
--l2 = list (lit 2) (labs $ \_ -> unsized)
--l00 = list (lit 0) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
--l10 = list (lit 1) (labs $ \_ -> list (lit 0) (labs $ \_ -> unsized))
--l01 = list (lit 0) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
--l11 = list (lit 1) (labs $ \_ -> list (lit 1) (labs $ \_ -> unsized))
--l12 = list (lit 1) (labs $ \_ -> list (lit 2) (labs $ \_ -> unsized))