lazy-lambda-calculus: be5ffc6e5355091df0a57c4f6ab228d9b809f5bb

     1: module Data.Language.LC.Self where
     2: 
     3: import Debug.Trace
     4: 
     5: import Control.Monad.Partial
     6: import Data.Language.LC
     7: import Data.Nat
     8: import Data.Typeable
     9: 
    10: -- Lambda calculus inside lambda calculus, using Morgensen-Scott encoding
    11: 
    12: decode :: (Encodable a) => Term a -> Partial (Val a)
    13: decode = (>>= unmse) . eval
    14: 
    15: extractC :: Partial (Val a) -> Partial (Maybe a)
    16: extractC = let f (C x) = Just x
    17:                f  _    = Nothing in
    18:            fmap f
    19: 
    20: class (Typeable a) => Encodable a where
    21:   mse   :: a -> Term  b
    22:   unmse :: (Typeable b) => Val b -> Partial (Val a)
    23: 
    24: instance Encodable () where
    25:   mse  () = Lam 0
    26:   unmse x = cast' x >>= ($$ ())
    27: 
    28: instance Encodable Bool where
    29:   mse True  = Lam (Lam 1)
    30:   mse False = Lam (Lam 0)
    31:   unmse x = cast' x >>= ($$ True) >>= ($$ False)
    32: 
    33: instance Encodable Nat where
    34:   mse x = let wrap Z = 1
    35:               wrap (S n) = 0 :@ wrap n in
    36:           Lam (Lam (wrap x))
    37: 
    38:   unmse x = eval' (0 :@ 1 :@ 2) [cast' x, Now (C 0), Now (F (fmap (valMap S)))]
    39: {-
    40: instance (Encodable a, Show a) => Encodable (Partial a) where
    41:   mse (Now   x) = Lam (Lam (1 :@ mse x))
    42:   mse (Later x) = Lam (Lam (0 :@ mse x))
    43: 
    44:   unmse x = eval' (0 :@ 1 :@ 2) [Now x,
    45:                                  Now (F (\y -> do y'    <- y
    46:                                                   C y'' <- unmse y'
    47:                                                   return (C y''))),
    48:                                  Now (F (fmap (valMap Later)))]
    49: 
    50: instance Encodable a => Encodable [a] where
    51:   mse []     = Lam (Lam 1)
    52:   mse (x:xs) = Lam (Lam (0 :@ mse x :@ mse xs))
    53: 
    54: instance Encodable a  => Encodable (Term a) where
    55:   mse (Const x) = Lam (Lam (Lam (Lam (3 :@ mse x))))
    56:   mse (Var   n) = Lam (Lam (Lam (Lam (2 :@ mse n))))
    57:   mse (Lam   f) = Lam (Lam (Lam (Lam (1 :@ mse f))))
    58:   mse (l :@  r) = Lam (Lam (Lam (Lam (0 :@ mse l :@ mse r))))
    59: 
    60: {-
    61: Lookup an element in a List. We can ignore empty lists:
    62: 
    63: selfLookup (h:t)  Z    = h
    64: selfLookup (h:t) (S n) = selfLookup t n
    65: 
    66: We can abstract out the recursion using a Z combinator:
    67: 
    68: selfLookup = let f g (h:t)  Z    = h
    69:                  f g (h:t) (S n) = g t n in
    70:              zComb f
    71: 
    72: By definition '(h:t) A B = B h t', which eliminates the pattern-match:
    73: 
    74: selfLookup = let f g l  Z    = l id (\a b -> a)
    75:                  f g l (S n) = l id (\a b -> g b n) in
    76:              zComb f
    77: 
    78: By definition 'Z A B = A' and '(S n) A B = B n', which eliminates the remaining
    79: pattern-match:
    80: 
    81: selfLookup = let f g l m = m (l id (\a b -> a))
    82:                              (\n -> l id (\a b -> g b n)) in
    83:              zComb f
    84: 
    85: Now we can put everything inline:
    86: 
    87: selfLookup = zComb (\g l m -> m (l id (\a b -> a))
    88:                                 (\n -> l id (\a b -> g b n)))
    89: 
    90: -}
    91: selfLookup = let z = 1 :@ mse () :@ mse Z
    92:                  s = Lam (2 :@ mse () :@ Lam (Lam (5 :@ 0 :@ 2))) in
    93:              zComb :@ Lam (Lam (Lam (0 :@ z :@ s)))
    94: -}