Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# LANGUAGE DataKinds #-}
- {-# LANGUAGE GADTs #-}
- {-# LANGUAGE StandaloneDeriving #-}
- {-# LANGUAGE TypeOperators #-}
- module Typed where
- import Prelude hiding (Left, Right, fst, snd)
- data Elem as a where
- EZ :: Elem (a:as) a
- ES :: Elem as a -> Elem (b:as) a
- instance Show (Elem as a) where
- show EZ = show 0
- show (ES x) = show (1 + read (show x))
- data Expr as a where
- Ref :: Elem as a -> Expr as a
- Abs :: Expr (a:as) b -> Expr as (a -> b)
- App :: Expr as (a -> b) -> Expr as a -> Expr as b
- Pair :: Expr as a -> Expr as b -> Expr as (a, b)
- Fst :: Expr as (a, b) -> Expr as a
- Snd :: Expr as (a, b) -> Expr as b
- InL :: Expr as a -> Expr as (Either a b)
- InR :: Expr as b -> Expr as (Either a b)
- Case :: Expr as (Either a b) -> Expr (a:as) c -> Expr (b:as) c -> Expr as c
- Num :: Integer -> Expr as Integer
- Bool :: Bool -> Expr as Bool
- deriving instance Show (Expr as a)
- data Value a where
- Closure :: Env as -> Expr as (a -> b) -> Value (a -> b)
- Tuple :: Value a -> Value b -> Value (a, b)
- Left :: Value a -> Value (Either a b)
- Right :: Value b -> Value (Either a b)
- Number :: Integer -> Value Integer
- Boolean :: Bool -> Value Bool
- deriving instance Show (Value a)
- fst :: Value (a, b) -> Value a
- fst (Tuple x _) = x
- snd :: Value (a, b) -> Value b
- snd (Tuple _ x) = x
- data Env as where
- Empty :: Env '[]
- Cons :: Value a -> Env as -> Env (a:as)
- deriving instance Show (Env as)
- get :: Elem as a -> Env as -> Value a
- get EZ (Cons x _) = x
- get (ES x) (Cons _ xs) = get x xs
- eval :: Expr '[] a -> Value a
- eval x = go Empty x
- where go :: Env as -> Expr as a -> Value a
- go env (Ref x) = get x env
- go env (Abs x) = Closure env (Abs x)
- go env (App x y) = apply (go env x) (go env y)
- go env (Pair x y) = Tuple (go env x) (go env y)
- go env (Fst x) = fst $ go env x
- go env (Snd x) = snd $ go env x
- go env (InL x) = Left (go env x)
- go env (InR x) = Right (go env x)
- go env (Case x left right) =
- case (go env x) of
- Left x -> go (Cons x env) left
- Right x -> go (Cons x env) right
- go _ (Num x) = Number x
- go _ (Bool x) = Boolean x
- apply :: Value (a -> b) -> Value a -> Value b
- apply (Closure env (Abs body)) x = go (Cons x env) body
- apply _ _ = undefined
- s :: Expr as ((a -> b -> c) -> (a -> b) -> a -> c)
- s = Abs (Abs (Abs (App (App (Ref (ES (ES EZ))) (Ref EZ)) (App (Ref (ES EZ)) (Ref EZ)))))
- k :: Expr as (a -> b -> a)
- k = Abs (Abs (Ref (ES EZ)))
- i :: Expr as (a -> a)
- i = Abs (Ref EZ)
- -- eval $ s `App` k `App` k
- -- eval $ s `App` k `App` k `App` Num 10
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement