lazy-lambda-calculus: 401e25a58c5b3fb2d37b10c3b32ac9f37a9b3cd9

     1: {-# Language FlexibleInstances          #-}
     2: {-# Language MultiParamTypeClasses      #-}
     3: {-# Language DeriveDataTypeable         #-}
     4: 
     5: module Data.Language.LC where
     6: 
     7: import Control.Monad.Partial
     8: import Data.Nat
     9: import Data.Data
    10: import Data.Typeable
    11: 
    12: -- Lambda calculus terms, with De Bruijn indices and opaque constants
    13: data Term a = Const a
    14:             | Var Nat
    15:             | Lam (Term a)
    16:             | Term a :@ Term a
    17:               deriving (Show, Typeable, Data)
    18: 
    19: -- This lets us abbreviate "Var 0", "Var 1", etc. to "0" "1", etc.
    20: instance Num (Term a) where
    21:   (+)    = error "Cannot add Terms"
    22:   (-)    = error "Cannot subtract Terms"
    23:   (*)    = error "Cannot multiply Terms"
    24:   abs    = error "Cannot abs a Term"
    25:   negate = error "Cannot negate a Term"
    26:   signum = error "Cannot signum a Term"
    27:   fromInteger = Var . fromInteger
    28: 
    29: instance Eq a => Eq (Term a) where
    30:   (Const x)  == (Const y)  = x == y
    31:   (Var   x)  == (Var   y)  = x == y
    32:   (Lam   x)  == (Lam   y)  = x == y
    33:   (l1 :@ r1) == (l2 :@ r2) = l1 == l2 && r1 == r2
    34: 
    35: -- The results of evaluation: either a value or a closure
    36: data Val a = C a
    37:            | F (Partial (Val a) -> Partial (Val a))
    38: 
    39: instance Show a => Show (Val a) where
    40:   show (C x) = "(C " ++ show x ++ ")"
    41:   show (F f) = "(F <function>)"
    42: 
    43: instance Eq a => Eq (Val a) where
    44:   (C x) == (C y) = x == y
    45:   (F x) == (F y) = error "Cannot compare function Vals"
    46:   _     == _     = False
    47: 
    48: instance Functor Val where
    49:   fmap f (C x) = C (f x)
    50:   fmap f (F g) = error "Cannot map embedded function"
    51: 
    52: valMap :: (a -> b) -> Val a -> Val b
    53: valMap f (C x) = C (f x)
    54: valMap f (F g) = error "Cannot map over function"
    55: 
    56: valLift :: (a -> a) -> Val a
    57: valLift f = F (fmap (fmap f))
    58: 
    59: liftVal :: Val a -> Val (Either b a)
    60: liftVal (C x) = C (Right x)
    61: liftVal (F f) = F (fmap liftVal . f . fmap lowerVal)
    62: 
    63: lowerVal :: Val (Either a b) -> Val b
    64: lowerVal (C (Right x)) = C x
    65: lowerVal (F f) = F (fmap lowerVal . f . fmap liftVal)
    66: 
    67: flipVal :: Val (Either a b) -> Val (Either b a)
    68: flipVal (C (Left  x)) = C (Right x)
    69: flipVal (C (Right x)) = C (Left  x)
    70: flipVal (F f)         = F (fmap flipVal . f . fmap flipVal)
    71: 
    72: -- Apply a function Val to an argument
    73: ($$) (F f) x = f (Now (C x))
    74: ($$) (C f) x = error "Cannot apply C as a function"
    75: 
    76: -- Evaluation environment
    77: type Env a = [Partial (Val a)]
    78: 
    79: -- Fully evaluates a Term, using Partial to handle nontermination
    80: eval' :: Term a -> Env a -> Partial (Val a)
    81: eval' (Const c) env = Now (C c)
    82: eval' (Var   n) env = let Just x = lookUp env n in x
    83: eval' (Lam   f) env = Now (F (\a -> eval' f (a:env)))
    84: eval' (f :@  x) env = do F f' <- eval' f env
    85:                          Later (f' (eval' x env))
    86: 
    87: -- Entry point for eval'
    88: eval t | closed t = eval' t []
    89: eval t            = error "Can only evaluate closed Terms"
    90: 
    91: -- Abbreviation for performing N steps
    92: evalN n = force n . eval
    93: 
    94: -- Predicate for capping the number of free variables in a Term
    95: freeVars :: Nat -> Term a -> Bool
    96: freeVars n (Const _) = True
    97: freeVars n (Var   m) = m < n
    98: freeVars n (Lam   f) = freeVars (S n) f
    99: freeVars n (l :@ r)  = freeVars n l && freeVars n r
   100: 
   101: -- Predicate for ensuring a Term has no free variables
   102: closed :: Term a -> Bool
   103: closed = freeVars 0
   104: 
   105: castTerm :: Term a -> Term b
   106: castTerm (Const x) = error "Cannot cast Constants"
   107: castTerm (Var   n) = Var n
   108: castTerm (Lam   f) = Lam (castTerm f)
   109: castTerm (l :@  r) = castTerm l :@ castTerm r
   110: 
   111: -- Infinite loop
   112: omega = Lam (0 :@ 0) :@ Lam (0 :@ 0)
   113: 
   114: -- Y combinator
   115: yComb = Lam (Lam (1 :@ (0 :@ 0)) :@ Lam (1 :@ (0 :@ 0)))
   116: 
   117: -- Z combinator
   118: zComb = Lam (Lam (1 :@ Lam (1 :@ 1 :@ 0)) :@ Lam (1 :@ Lam (1 :@ 1 :@ 0)))