Skip to content

Instantly share code, notes, and snippets.

@gallais
Created May 4, 2014
Embed
What would you like to do?
{-# LANGUAGE GADTs#-}
data Lam a where
Var :: a -> Lam a
App :: Lam a -> Lam a -> Lam a
Lam :: Lam (Maybe a) -> Lam a
mapLam :: (a -> b) -> Lam a -> Lam b
mapLam f (Var a) = Var $ f a
mapLam f (App t u) = mapLam f t `App` mapLam f u
mapLam f (Lam b) = Lam $ mapLam (fmap f) b
betaRedOk :: Lam (Maybe Int) -> Lam Int -> Lam Int
betaRedOk b u =
let f = mapLam id
in App (Lam $ f b) (f u)
betaRedFail :: Lam (Maybe Int) -> Lam Int -> Lam Int
betaRedFail b u = (\ f -> App (Lam $ f b) (f u)) $ mapLam id
{-
NoMono.hs:19:44:
Couldn't match type `Maybe Int' with `Int'
Expected type: Lam Int
Actual type: Lam (Maybe Int)
In the return type of a call of `f'
In the second argument of `App', namely `(f u)'
In the expression: App (Lam $ f b) (f u)
NoMono.hs:19:46:
Couldn't match type `Int' with `Maybe Int'
Expected type: Lam (Maybe Int)
Actual type: Lam Int
In the first argument of `f', namely `u'
In the second argument of `App', namely `(f u)'
In the expression: App (Lam $ f b) (f u)
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment