Skip to content

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Typed concatenative language implemented with type level lists.
-- Type level implementation of OCaml code from
-- http://alaska-kamtchatka.blogspot.com/2009/01/essence-of-concatenative-languages.html
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
infixl 4 :->
infixr 5 :-
data TType = TInt | TBol | [TType] :-> [TType]
type family TTypeT (t :: TType) :: *
type instance TTypeT TInt = Int
type instance TTypeT TBol = Bool
type instance TTypeT (r :-> s) = RTypeT r -> RTypeT s
data family RTypeT (r :: [TType]) :: *
data instance RTypeT (t ': r) = TTypeT t :- RTypeT r
data instance RTypeT '[] = E
data Term :: [TType] -> [TType] -> * where
Id :: Term r r
I :: Int -> Term r (TInt ': r)
B :: Bool -> Term r (TBol ': r)
Q :: Term s t -> Term r ((s :-> t) ': r)
(:<) :: Term r s -> Term s t -> Term r t
PAdd :: Term (TInt ': TInt ': r) (TInt ': r)
PCompose :: Term ((t :-> u) ': (s :-> t) ': r) ((s :-> u) ': r)
eval :: Term r s -> RTypeT r -> RTypeT s
eval Id r = r
eval (I i) r = i :- r
eval (B b) r = b :- r
eval (Q q) r = eval q :- r
eval (a :< b) r = eval b (eval a r)
eval PAdd (i :- j :- r) = i + j :- r
eval PCompose (f :- g :- r) = f . g :- r
run :: Term '[] r -> RTypeT r
run t = eval t E
-- GHC can infer this type:
test :: Term r ((TInt ': s :-> TInt ': s) ': r)
test = Q (I 42) :< Q PAdd :< PCompose
test1 = case run test of
f :- E -> case (f (1 :- E)) of
x :- E -> x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.