lambda/bug.icl

   1 module test
   2
   3 import StdEnv
   4
   5 :: Either l r = Left l | Right r
   6 either f _ (Left x) = f x
   7 either _ f (Right x) = f x
   8 class Functor m
   9 where
  10         fmap :: (a -> b) (m a) -> m b
  11         (<$>) infixl 4 :: (a -> b) (m a) -> m b
  12         (<$>) a b = fmap a b
  13 class Applicative m
  14 where
  15         pure :: a -> m a
  16         (<*>) infixl 4 :: (m (a -> b)) (m a) -> m b
  17 class Monad m
  18 where
  19         bind :: (m a) (a -> m b) -> m b
  20         (>>=) infixl 1 :: (m a) (a -> m b) -> m b
  21         (>>=) a b = bind a b
  22         (>>|) infixl 1 :: (m a) (m b) -> m b
  23         (>>|) a b = bind a \_->b
  24
  25 :: In a b = In infixl 0 a b
  26 class lambda v
  27 where
  28         (@) infixr 1 :: (v (a -> v b)) (v a) -> v b
  29         \| :: ((v a) -> v b) -> v (a -> v b) | TC a & TC b & TC (v b)
  30
  31 class expr v
  32 where
  33         lit :: a -> v a | toString a
  34         (+.) infixl 6 :: (v a) (v a) -> v a | + a
  35         (-.) infixl 6 :: (v a) (v a) -> v a | - a
  36         (*.) infixl 6 :: (v a) (v a) -> v a | * a
  37         (/.) infixl 6 :: (v a) (v a) -> v a | / a
  38         (==.) infix 4 :: (v a) (v a) -> v Bool | == a
  39         If :: (v Bool) (v a) (v a) -> v a
  40
  41 class let v
  42 where
  43         lett :: ((v a) -> In (v a) (v b)) -> v b | TC a
  44
  45 :: St a = St (Env -> Either String (a, Env))
  46 :: Env :== [Dynamic]
  47 instance Functor St where fmap f m = m >>= \a->pure (f a)
  48 instance Applicative St
  49 where
  50         pure x = St \s->Right (x, s)
  51         (<*>) mfa ma = mfa >>= \fa->ma >>= \a->pure (fa a)
  52 instance Monad St
  53 where
  54         bind ma a2mb = St \s->case evalSt ma s of
  55                 Left err = Left err
  56                 Right (a, s) = evalSt (a2mb a) s
  57
  58 get   = St \s->Right (s, s)
  59 put s = St \_->Right ((), s)
  60 fail e = St \_->Left e
  61 evalSt (St m) = m
  62 eval m = either Left (Right o fst) (evalSt m [])
  63
  64 instance expr St
  65 where
  66         lit a = pure a
  67         (+.) l r = (+) <$> l <*> r
  68         (-.) l r = (-) <$> l <*> r
  69         (*.) l r = (*) <$> l <*> r
  70         (/.) l r = (/) <$> l <*> r
  71         (==.) l r = (==) <$> l <*> r
  72         If i t e = i >>= \b->if b t e
  73
  74 instance lambda St
  75 where
  76         (@) l r = l >>= \l->r >>= \r->l r
  77         \| def = pure (def o pure)
  78
  79 instance let St
  80 where
  81         lett def = length <$> get >>= \l->
  82                 let (x In y) = def (get >>= deref o flip (!!) l)
  83                 in  get >>= \s->put (s ++ [dynamic x]) >>| y
  84
  85 deref a = abort (toString (typeCodeOfDynamic a))
  86 deref (a :: a^) = a
  87 deref _ = fail "Variable not known???"
  88
  89 :: Print a = Print (Int [String] -> [String])
  90 unPrint (Print f) = f
  91 print :: (Print a) -> [String]
  92 print f = unPrint f 0 []
  93 var d i _ c = [d,toString i:c]
  94 instance expr Print
  95 where
  96         lit a = Print \i c->[toString a:c]
  97         (+.) l r = Print \i c->["(":unPrint l i ["+":unPrint r i [")":c]]]
  98         (-.) l r = Print \i c->["(":unPrint l i ["-":unPrint r i [")":c]]]
  99         (*.) l r = Print \i c->["(":unPrint l i ["*":unPrint r i [")":c]]]
 100         (/.) l r = Print \i c->["(":unPrint l i ["/":unPrint r i [")":c]]]
 101         (==.) l r = Print \i c->["(":unPrint l i ["==":unPrint r i [")":c]]]
 102         If p t e = Print \i c->["if ":unPrint p i [" ":unPrint t i [" ":unPrint e i c]]]
 103 instance lambda Print
 104 where
 105         (@) l r = Print \i c->["(":unPrint l i [" ":unPrint r i [")":c]]]
 106         \| def = Print \i c->["(\\":var "x" i i ["->":unPrint (def (Print (var "x" i))) (inc i) [")":c]]]
 107 instance let Print
 108 where
 109         lett def = Print \i c->let (x In y) = def (Print (var "f" i))
 110                 in ["(let ":var "f" i i ["=":unPrint x i ["\nin ":unPrint y (inc i) [")":c]]]]
 111
 112 Start =
 113         ( "--eval t1: ", eval t1
 114         , "\n--print t1:\n", print t1
 115         , "--eval t2: ", eval t2
 116         , "\n--pritn t2:\n", print t2
 117         )
 118
 119 t1 :: (v Int) | let, lambda, expr v & TC (v Int)
 120 t1 =
 121            lett \id     = (\| \x->x)
 122         In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
 123         In fac @ id @ lit 10
 124
 125 t2 :: (v Int) | let, lambda, expr v & TC (v Int) & TC (v (Int -> v Int))
 126 t2 =
 127            lett \id     = (\| \x->x)
 128         In lett \fix    = (\| \f->lett \x=f @ x In x)
 129         In lett \fac    = (\| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1)))
 130         In lett \facfix = (\| \n->(fix @ \| \fac-> \| \n->If (n ==. lit 0) (lit 1) (n *. (fac @ n -. lit 1))) @ n)
 131         In facfix @ id @ lit 10