Mixing
Haskell Interpreter for System T Combinator Language
In a previous question SystemT Compiler and dealing with Infinite Types in Haskell I asked about how to parse a SystemT Lambda Calculus to SystemT Combinators. I decided to use plain algebraic data types for encoding both the SystemT Lambda calculus and SystemT Combinator calculus (based on the comment: SystemT Compiler and dealing with Infinite Types in Haskell).
SystemTCombinator.hs:
module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)
SystemTLambda.hs:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SystemTLambda where
import Control.Monad.Catch
import Data.Either (fromRight)
import qualified SystemTCombinator as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ ctx ->
either Left (v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ ctx -> Right a
fs <*> xs = Parser $ ctx ->
either Left (f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ ctx ->
either Left (v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ ctx ->
either
(e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= ((varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _ _ ) ttype = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _ _ ) ttype = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
( "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"
I use the above bidirectional type checker to parse SystemTLambda.TTerm into SystemTCombinator.THom.
systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result)
The combinator expression is:
Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)
The problem I have now is how to interpret this combinator expression. I know that all combinator expressions are meant to be interpreted as a function. The problem is that I don't know the input and output types of this function, and I expect that the "interpreter" function will be partial, in that if it tries to interpret something incorrectly it should result in a RuntimeException because the combinator expression is untyped, it is possible to have bad combinator expressions. However my type checker should ensure that once reaching the interpreter the combinators should be well typed already.
According to the original blog post, http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html the combinators have all functional equivalents. Something like:
evaluate Id = id
evaluate Unit = const ()
evaluate Zero = () -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = (f, v) -> f v
evaluate (Iter base recurse) = (a, n) ->
case n of
Z -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))
But obviously that doesn't work. It seems that there must be some way of interpreting the THom tree, such that I get some sort of function back, that can be executed in partial manner.
haskell ocaml interpreter lambda-calculus combinatory-logic
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
add a comment |
In a previous question SystemT Compiler and dealing with Infinite Types in Haskell I asked about how to parse a SystemT Lambda Calculus to SystemT Combinators. I decided to use plain algebraic data types for encoding both the SystemT Lambda calculus and SystemT Combinator calculus (based on the comment: SystemT Compiler and dealing with Infinite Types in Haskell).
SystemTCombinator.hs:
module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)
SystemTLambda.hs:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SystemTLambda where
import Control.Monad.Catch
import Data.Either (fromRight)
import qualified SystemTCombinator as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ ctx ->
either Left (v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ ctx -> Right a
fs <*> xs = Parser $ ctx ->
either Left (f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ ctx ->
either Left (v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ ctx ->
either
(e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= ((varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _ _ ) ttype = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _ _ ) ttype = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
( "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"
I use the above bidirectional type checker to parse SystemTLambda.TTerm into SystemTCombinator.THom.
systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result)
The combinator expression is:
Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)
The problem I have now is how to interpret this combinator expression. I know that all combinator expressions are meant to be interpreted as a function. The problem is that I don't know the input and output types of this function, and I expect that the "interpreter" function will be partial, in that if it tries to interpret something incorrectly it should result in a RuntimeException because the combinator expression is untyped, it is possible to have bad combinator expressions. However my type checker should ensure that once reaching the interpreter the combinators should be well typed already.
According to the original blog post, http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html the combinators have all functional equivalents. Something like:
evaluate Id = id
evaluate Unit = const ()
evaluate Zero = () -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = (f, v) -> f v
evaluate (Iter base recurse) = (a, n) ->
case n of
Z -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))
But obviously that doesn't work. It seems that there must be some way of interpreting the THom tree, such that I get some sort of function back, that can be executed in partial manner.
haskell ocaml interpreter lambda-calculus combinatory-logic
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer ofTHomterms to your target language answer your question (in which case a description of said language seems necessary)?
– Li-yao Xia
Jan 1 at 17:41
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15
add a comment |
In a previous question SystemT Compiler and dealing with Infinite Types in Haskell I asked about how to parse a SystemT Lambda Calculus to SystemT Combinators. I decided to use plain algebraic data types for encoding both the SystemT Lambda calculus and SystemT Combinator calculus (based on the comment: SystemT Compiler and dealing with Infinite Types in Haskell).
SystemTCombinator.hs:
module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)
SystemTLambda.hs:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SystemTLambda where
import Control.Monad.Catch
import Data.Either (fromRight)
import qualified SystemTCombinator as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ ctx ->
either Left (v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ ctx -> Right a
fs <*> xs = Parser $ ctx ->
either Left (f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ ctx ->
either Left (v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ ctx ->
either
(e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= ((varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _ _ ) ttype = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _ _ ) ttype = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
( "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"
I use the above bidirectional type checker to parse SystemTLambda.TTerm into SystemTCombinator.THom.
systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result)
The combinator expression is:
Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)
The problem I have now is how to interpret this combinator expression. I know that all combinator expressions are meant to be interpreted as a function. The problem is that I don't know the input and output types of this function, and I expect that the "interpreter" function will be partial, in that if it tries to interpret something incorrectly it should result in a RuntimeException because the combinator expression is untyped, it is possible to have bad combinator expressions. However my type checker should ensure that once reaching the interpreter the combinators should be well typed already.
According to the original blog post, http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html the combinators have all functional equivalents. Something like:
evaluate Id = id
evaluate Unit = const ()
evaluate Zero = () -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = (f, v) -> f v
evaluate (Iter base recurse) = (a, n) ->
case n of
Z -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))
But obviously that doesn't work. It seems that there must be some way of interpreting the THom tree, such that I get some sort of function back, that can be executed in partial manner.
haskell ocaml interpreter lambda-calculus combinatory-logic
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
In a previous question SystemT Compiler and dealing with Infinite Types in Haskell I asked about how to parse a SystemT Lambda Calculus to SystemT Combinators. I decided to use plain algebraic data types for encoding both the SystemT Lambda calculus and SystemT Combinator calculus (based on the comment: SystemT Compiler and dealing with Infinite Types in Haskell).
SystemTCombinator.hs:
module SystemTCombinator where
data THom = Id
| Unit
| Zero
| Succ
| Compose THom THom
| Pair THom THom
| Fst
| Snd
| Curry THom
| Eval
| Iter THom THom
deriving (Show)
SystemTLambda.hs:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SystemTLambda where
import Control.Monad.Catch
import Data.Either (fromRight)
import qualified SystemTCombinator as SystemTC
type TVar = String
data TType = One | Prod TType TType | Arrow TType TType | Nat deriving (Eq)
instance Show TType where
show ttype = case ttype of
One -> "'Unit"
Nat -> "'Nat"
Prod ttype1 ttype2 ->
"(" ++ show ttype1 ++ " * " ++ show ttype2 ++ ")"
Arrow ttype1@(Arrow _ _) ttype2 ->
"(" ++ show ttype1 ++ ") -> " ++ show ttype2
Arrow ttype1 ttype2 -> show ttype1 ++ " -> " ++ show ttype2
data TTerm = Var TVar
| Let TVar TTerm TTerm
| Lam TVar TTerm
| App TTerm TTerm
| Unit
| Pair TTerm TTerm
| Fst TTerm
| Snd TTerm
| Zero
| Succ TTerm
| Iter TTerm TTerm TVar TTerm
| Annot TTerm TType
deriving (Show)
-- a context is a list of hypotheses/judgements
type TContext = [(TVar, TType)]
-- our exceptions for SystemT
data TException = TypeCheckException String
| BindingException String
deriving (Show)
instance Exception TException
newtype Parser a = Parser { run :: TContext -> Either SomeException a }
instance Functor Parser where
fmap f xs = Parser $ ctx ->
either Left (v -> Right $ f v) $ run xs ctx
instance Applicative Parser where
pure a = Parser $ ctx -> Right a
fs <*> xs = Parser $ ctx ->
either Left (f -> fmap f $ run xs ctx) (run fs ctx)
instance Monad Parser where
xs >>= f = Parser $ ctx ->
either Left (v -> run (f v) ctx) $ run xs ctx
instance MonadThrow Parser where
throwM e = Parser (const $ Left $ toException e)
instance MonadCatch Parser where
catch p f = Parser $ ctx ->
either
(e -> case fromException e of
Just e' -> run (f e') ctx -- this handles the exception
Nothing -> Left e) -- this propagates it upwards
Right
$ run p ctx
withHypothesis :: (TVar, TType) -> Parser a -> Parser a
withHypothesis hyp cmd = Parser $ ctx -> run cmd (hyp : ctx)
tvarToHom :: TVar -> Parser (SystemTC.THom, TType)
tvarToHom var = Parser $ ctx ->
case foldr transform Nothing ctx of
Just x -> Right x
Nothing -> throwM $ BindingException ("unbound variable " ++ show var)
where
transform (var', varType) homAndType =
if var == var'
then Just (SystemTC.Snd, varType)
else homAndType >>= ((varHom, varType) -> Just (SystemTC.Compose SystemTC.Fst varHom, varType))
check :: TTerm -> TType -> Parser SystemTC.THom
-- check a lambda
check (Lam var bodyTerm) (Arrow varType bodyType) =
withHypothesis (var, varType) $
check bodyTerm bodyType >>= (bodyHom -> return $ SystemTC.Curry bodyHom)
check (Lam _ _ ) ttype = throwM
$ TypeCheckException ("expected function type, got '" ++ show ttype ++ "'")
-- check unit
check Unit One = return SystemTC.Unit
check Unit ttype =
throwM $ TypeCheckException ("expected unit type, got '" ++ show ttype ++ "'")
-- check products
check (Pair term1 term2) (Prod ttype1 ttype2) = do
hom1 <- check term1 ttype1
hom2 <- check term2 ttype2
return $ SystemTC.Pair hom1 hom2
check (Pair _ _ ) ttype = throwM
$ TypeCheckException ("expected product type, got '" ++ show ttype ++ "'")
-- check primitive recursion
check (Iter baseTerm inductTerm tvar numTerm) ttype = do
baseHom <- check baseTerm ttype
inductHom <- withHypothesis (tvar, ttype) (check inductTerm ttype)
numHom <- check numTerm Nat
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id numHom)
(SystemTC.Iter baseHom inductHom)
-- check let bindings
check (Let var valueTerm exprTerm) exprType = do
(valueHom, valueType) <- synth valueTerm
exprHom <- withHypothesis (var, valueType) (check exprTerm exprType)
return $ SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom
check tterm ttype = do
(thom, ttype') <- synth tterm
if ttype == ttype'
then return thom
else throwM $ TypeCheckException
( "expected type '"
++ show ttype
++ "', inferred type '"
++ show ttype'
++ "'"
)
synth :: TTerm -> Parser (SystemTC.THom, TType)
synth (Var tvar) = tvarToHom tvar
synth (Let var valueTerm exprTerm) = do
(valueHom, valueType) <- synth valueTerm
(exprHom, exprType) <- withHypothesis (var, valueType) (synth exprTerm)
return (SystemTC.Compose (SystemTC.Pair SystemTC.Id valueHom) exprHom, exprType)
synth (App functionTerm valueTerm) = do
(functionHom, functionType) <- synth functionTerm
case functionType of
Arrow headType bodyType -> do
valueHom <- check valueTerm headType
return (SystemTC.Compose (SystemTC.Pair functionHom valueHom) SystemTC.Eval, bodyType)
_ -> throwM $ TypeCheckException ("expected function, got '" ++ show functionType ++ "'")
synth (Fst pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Fst, fstType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth (Snd pairTerm) = do
(pairHom, pairType) <- synth pairTerm
case pairType of
Prod fstType sndType -> return (SystemTC.Compose pairHom SystemTC.Snd, sndType)
_ -> throwM $ TypeCheckException ("expected product, got '" ++ show pairType ++ "'")
synth Zero = return (SystemTC.Compose SystemTC.Unit SystemTC.Zero, Nat)
synth (Succ numTerm) = do
numHom <- check numTerm Nat
return (SystemTC.Compose numHom SystemTC.Succ, Nat)
synth (Annot term ttype) = do
hom <- check term ttype
return (hom, ttype)
synth _ = throwM $ TypeCheckException "unknown synthesis"
I use the above bidirectional type checker to parse SystemTLambda.TTerm into SystemTCombinator.THom.
systemTLambda :: TTerm
systemTLambda =
Let "sum"
(Annot
(Lam "x" $ Lam "y" $
Iter (Var "y") (Succ $ Var "n") "n" (Var "x"))
(Arrow Nat $ Arrow Nat Nat))
(App
(App
(Var "sum")
(Succ $ Succ Zero))
(Succ $ Succ $ Succ Zero))
systemTCombinator :: Either SomeException (SystemTC.THom, SystemTC.TType)
systemTCombinator = fromRight Unit $ run (synth result)
The combinator expression is:
Compose (Pair Id (Curry (Curry (Compose (Pair Id (Compose Fst Snd)) (Iter Snd (Compose Snd Succ)))))) (Compose (Pair (Compose (Pair Snd (Compose (Compose (Compose Unit Zero) Succ) Succ)) Eval) (Compose (Compose (Compose (Compose Unit Zero) Succ) Succ) Succ)) Eval)
The problem I have now is how to interpret this combinator expression. I know that all combinator expressions are meant to be interpreted as a function. The problem is that I don't know the input and output types of this function, and I expect that the "interpreter" function will be partial, in that if it tries to interpret something incorrectly it should result in a RuntimeException because the combinator expression is untyped, it is possible to have bad combinator expressions. However my type checker should ensure that once reaching the interpreter the combinators should be well typed already.
According to the original blog post, http://semantic-domain.blogspot.com/2012/12/total-functional-programming-in-partial.html the combinators have all functional equivalents. Something like:
evaluate Id = id
evaluate Unit = const ()
evaluate Zero = () -> Z
evaluate (Succ n) = S n
evaluate (Compose f g) = (evaluate g) . (evaluate f)
evaluate (Pair l r) = (evaluate l, evaluate r)
evaluate Fst = fst
evaluate Snd = snd
evaluate (Curry h) = curry (evaluate h)
evaluate Eval = (f, v) -> f v
evaluate (Iter base recurse) = (a, n) ->
case n of
Z -> evaluate base a
S n -> evaluate recurse (a, evaluate (Iter base recurse) (a, n))
But obviously that doesn't work. It seems that there must be some way of interpreting the THom tree, such that I get some sort of function back, that can be executed in partial manner.
haskell ocaml interpreter lambda-calculus combinatory-logic
haskell ocaml interpreter lambda-calculus combinatory-logic
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
asked Jan 1 at 15:25
CMCDragonkaiCMCDragonkai
3,11363866
3,11363866
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer ofTHomterms to your target language answer your question (in which case a description of said language seems necessary)?
– Li-yao Xia
Jan 1 at 17:41
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15
add a comment |
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer ofTHomterms to your target language answer your question (in which case a description of said language seems necessary)?
– Li-yao Xia
Jan 1 at 17:41
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer of
THom terms to your target language answer your question (in which case a description of said language seems necessary)?– Li-yao Xia
Jan 1 at 17:41
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer of
THom terms to your target language answer your question (in which case a description of said language seems necessary)?– Li-yao Xia
Jan 1 at 17:41
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15
add a comment |
2 Answers
2
active
oldest
votes
To interpret THom in a guaranteed well-typed way, you will need to "explain" its types to the Haskell type checker. I see you have already considered the GADT version of THom, which would be the conventional way to do this explanation, and that's still the approach I would go with. If I understand correctly, the trouble you were facing is that the logic of synth was too complex to prove that it would always produce a well-typed THom, and this comes as no surprise.
I think you can keep your synth (rougly) as it is, if you add a simple pass that type checks the resulting untyped THom into a typed GADT, say StrongTHom a b. Returning existentials seems risky, it would be preferable to provide it an incoming context:
checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)
(where TType is the singleton form in the previous answer). It just requires you to know at the top level what your input and output types are going to be. This is usually fine, because in order to actually use the result you will eventually have to know the types at which it is instantiated anyway. (You might have to punt this expected type information outward a few levels until a concrete type is known)
If you absolutely must be able to infer the input and output types, then I suppose there is no choice but to return an existential. It just means that your type checker will include a lot more type equality checks (cf. typeEq below), and the untyped THom may also need to include more type information.
In either case THom will definitely have to include any types that it erases. For example, in Compose :: THom a b -> THom b c -> THom a c, b is erased and checkTHom will have to reconstruct it. So Compose needs to include enough information so that this is possible. At this point an existential (SomeType from the previous answer) will probably be fine, because the only way you have to use it is by unwrapping it and passing it on recursively.
To write this checker I have a feeling you will need a strong equality check:
typeEq :: TType a -> TType b -> Maybe (a :~: b)
(where :~: is standard type equality) which is easy to write; I'm just making sure you're aware of the technique.
Once you have this, then eval :: StrongTHom a b -> a -> b should go through like warm butter. Good luck!
answered Jan 1 at 19:55
luquiluqui
48k6114168
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggestedType a, how is it related toTType a?
– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADTValueof possible values, then you can interpret witheval :: THom -> Value -> Valueby pattern matching on both arguments. It is certainly a lot less trouble to do it that way.
– luqui
Jan 2 at 2:33
add a comment |
Alternatively, it is pretty easy to do runtime type checking by declaring a type of all possible values.
data Value
= VUnit -- of type One
| VPair Value Value -- of type Pair
| VFunc (Value -> Interp Value) -- of type Func
| VNat Integer -- of type Nat
Then you can very directly use your untyped THom, for an appropriate interpreter monad Interp (maybe just an Except monad):
eval :: THom -> Value -> Interp Value
eval Id v = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"
Notice also that VFunc above has the same type as the codomain of eval, since embedded functions may also fail.
answered Jan 2 at 2:41
luquiluqui
48k6114168
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53996638%2fhaskell-interpreter-for-system-t-combinator-language%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
To interpret THom in a guaranteed well-typed way, you will need to "explain" its types to the Haskell type checker. I see you have already considered the GADT version of THom, which would be the conventional way to do this explanation, and that's still the approach I would go with. If I understand correctly, the trouble you were facing is that the logic of synth was too complex to prove that it would always produce a well-typed THom, and this comes as no surprise.
I think you can keep your synth (rougly) as it is, if you add a simple pass that type checks the resulting untyped THom into a typed GADT, say StrongTHom a b. Returning existentials seems risky, it would be preferable to provide it an incoming context:
checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)
(where TType is the singleton form in the previous answer). It just requires you to know at the top level what your input and output types are going to be. This is usually fine, because in order to actually use the result you will eventually have to know the types at which it is instantiated anyway. (You might have to punt this expected type information outward a few levels until a concrete type is known)
If you absolutely must be able to infer the input and output types, then I suppose there is no choice but to return an existential. It just means that your type checker will include a lot more type equality checks (cf. typeEq below), and the untyped THom may also need to include more type information.
In either case THom will definitely have to include any types that it erases. For example, in Compose :: THom a b -> THom b c -> THom a c, b is erased and checkTHom will have to reconstruct it. So Compose needs to include enough information so that this is possible. At this point an existential (SomeType from the previous answer) will probably be fine, because the only way you have to use it is by unwrapping it and passing it on recursively.
To write this checker I have a feeling you will need a strong equality check:
typeEq :: TType a -> TType b -> Maybe (a :~: b)
(where :~: is standard type equality) which is easy to write; I'm just making sure you're aware of the technique.
Once you have this, then eval :: StrongTHom a b -> a -> b should go through like warm butter. Good luck!
answered Jan 1 at 19:55
luquiluqui
48k6114168
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggestedType a, how is it related toTType a?
– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADTValueof possible values, then you can interpret witheval :: THom -> Value -> Valueby pattern matching on both arguments. It is certainly a lot less trouble to do it that way.
– luqui
Jan 2 at 2:33
add a comment |
To interpret THom in a guaranteed well-typed way, you will need to "explain" its types to the Haskell type checker. I see you have already considered the GADT version of THom, which would be the conventional way to do this explanation, and that's still the approach I would go with. If I understand correctly, the trouble you were facing is that the logic of synth was too complex to prove that it would always produce a well-typed THom, and this comes as no surprise.
I think you can keep your synth (rougly) as it is, if you add a simple pass that type checks the resulting untyped THom into a typed GADT, say StrongTHom a b. Returning existentials seems risky, it would be preferable to provide it an incoming context:
checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)
(where TType is the singleton form in the previous answer). It just requires you to know at the top level what your input and output types are going to be. This is usually fine, because in order to actually use the result you will eventually have to know the types at which it is instantiated anyway. (You might have to punt this expected type information outward a few levels until a concrete type is known)
If you absolutely must be able to infer the input and output types, then I suppose there is no choice but to return an existential. It just means that your type checker will include a lot more type equality checks (cf. typeEq below), and the untyped THom may also need to include more type information.
In either case THom will definitely have to include any types that it erases. For example, in Compose :: THom a b -> THom b c -> THom a c, b is erased and checkTHom will have to reconstruct it. So Compose needs to include enough information so that this is possible. At this point an existential (SomeType from the previous answer) will probably be fine, because the only way you have to use it is by unwrapping it and passing it on recursively.
To write this checker I have a feeling you will need a strong equality check:
typeEq :: TType a -> TType b -> Maybe (a :~: b)
(where :~: is standard type equality) which is easy to write; I'm just making sure you're aware of the technique.
Once you have this, then eval :: StrongTHom a b -> a -> b should go through like warm butter. Good luck!
answered Jan 1 at 19:55
luquiluqui
48k6114168
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggestedType a, how is it related toTType a?
– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADTValueof possible values, then you can interpret witheval :: THom -> Value -> Valueby pattern matching on both arguments. It is certainly a lot less trouble to do it that way.
– luqui
Jan 2 at 2:33
add a comment |
To interpret THom in a guaranteed well-typed way, you will need to "explain" its types to the Haskell type checker. I see you have already considered the GADT version of THom, which would be the conventional way to do this explanation, and that's still the approach I would go with. If I understand correctly, the trouble you were facing is that the logic of synth was too complex to prove that it would always produce a well-typed THom, and this comes as no surprise.
I think you can keep your synth (rougly) as it is, if you add a simple pass that type checks the resulting untyped THom into a typed GADT, say StrongTHom a b. Returning existentials seems risky, it would be preferable to provide it an incoming context:
checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)
(where TType is the singleton form in the previous answer). It just requires you to know at the top level what your input and output types are going to be. This is usually fine, because in order to actually use the result you will eventually have to know the types at which it is instantiated anyway. (You might have to punt this expected type information outward a few levels until a concrete type is known)
If you absolutely must be able to infer the input and output types, then I suppose there is no choice but to return an existential. It just means that your type checker will include a lot more type equality checks (cf. typeEq below), and the untyped THom may also need to include more type information.
In either case THom will definitely have to include any types that it erases. For example, in Compose :: THom a b -> THom b c -> THom a c, b is erased and checkTHom will have to reconstruct it. So Compose needs to include enough information so that this is possible. At this point an existential (SomeType from the previous answer) will probably be fine, because the only way you have to use it is by unwrapping it and passing it on recursively.
To write this checker I have a feeling you will need a strong equality check:
typeEq :: TType a -> TType b -> Maybe (a :~: b)
(where :~: is standard type equality) which is easy to write; I'm just making sure you're aware of the technique.
Once you have this, then eval :: StrongTHom a b -> a -> b should go through like warm butter. Good luck!
answered Jan 1 at 19:55
luquiluqui
48k6114168
To interpret THom in a guaranteed well-typed way, you will need to "explain" its types to the Haskell type checker. I see you have already considered the GADT version of THom, which would be the conventional way to do this explanation, and that's still the approach I would go with. If I understand correctly, the trouble you were facing is that the logic of synth was too complex to prove that it would always produce a well-typed THom, and this comes as no surprise.
I think you can keep your synth (rougly) as it is, if you add a simple pass that type checks the resulting untyped THom into a typed GADT, say StrongTHom a b. Returning existentials seems risky, it would be preferable to provide it an incoming context:
checkTHom :: THom -> TType a -> TType b -> Maybe (StrongTHom a b)
(where TType is the singleton form in the previous answer). It just requires you to know at the top level what your input and output types are going to be. This is usually fine, because in order to actually use the result you will eventually have to know the types at which it is instantiated anyway. (You might have to punt this expected type information outward a few levels until a concrete type is known)
If you absolutely must be able to infer the input and output types, then I suppose there is no choice but to return an existential. It just means that your type checker will include a lot more type equality checks (cf. typeEq below), and the untyped THom may also need to include more type information.
In either case THom will definitely have to include any types that it erases. For example, in Compose :: THom a b -> THom b c -> THom a c, b is erased and checkTHom will have to reconstruct it. So Compose needs to include enough information so that this is possible. At this point an existential (SomeType from the previous answer) will probably be fine, because the only way you have to use it is by unwrapping it and passing it on recursively.
To write this checker I have a feeling you will need a strong equality check:
typeEq :: TType a -> TType b -> Maybe (a :~: b)
(where :~: is standard type equality) which is easy to write; I'm just making sure you're aware of the technique.
Once you have this, then eval :: StrongTHom a b -> a -> b should go through like warm butter. Good luck!
answered Jan 1 at 19:55
luquiluqui
48k6114168
edited Jan 2 at 2:32
answered Jan 1 at 19:55
luquiluqui
48k6114168
answered Jan 1 at 19:55
luquiluqui
48k6114168
answered Jan 1 at 19:55
luquiluqui
48k6114168
48k6114168
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggestedType a, how is it related toTType a?
– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADTValueof possible values, then you can interpret witheval :: THom -> Value -> Valueby pattern matching on both arguments. It is certainly a lot less trouble to do it that way.
– luqui
Jan 2 at 2:33
add a comment |
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggestedType a, how is it related toTType a?
– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADTValueof possible values, then you can interpret witheval :: THom -> Value -> Valueby pattern matching on both arguments. It is certainly a lot less trouble to do it that way.
– luqui
Jan 2 at 2:33
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Is it possible to have a partial intepreter? Would that be simpler solution?
– CMCDragonkai
Jan 2 at 2:04
Also your suggested
Type a, how is it related to TType a?– CMCDragonkai
Jan 2 at 2:11
Also your suggested
Type a, how is it related to TType a?– CMCDragonkai
Jan 2 at 2:11
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai it was just a ttypo
– luqui
Jan 2 at 2:32
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADT
Value of possible values, then you can interpret with eval :: THom -> Value -> Value by pattern matching on both arguments. It is certainly a lot less trouble to do it that way.– luqui
Jan 2 at 2:33
@CMCDragonkai Yeah a partial interpreter would just mean you should declare an ADT
Value of possible values, then you can interpret with eval :: THom -> Value -> Value by pattern matching on both arguments. It is certainly a lot less trouble to do it that way.– luqui
Jan 2 at 2:33
add a comment |
Alternatively, it is pretty easy to do runtime type checking by declaring a type of all possible values.
data Value
= VUnit -- of type One
| VPair Value Value -- of type Pair
| VFunc (Value -> Interp Value) -- of type Func
| VNat Integer -- of type Nat
Then you can very directly use your untyped THom, for an appropriate interpreter monad Interp (maybe just an Except monad):
eval :: THom -> Value -> Interp Value
eval Id v = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"
Notice also that VFunc above has the same type as the codomain of eval, since embedded functions may also fail.
answered Jan 2 at 2:41
luquiluqui
48k6114168
add a comment |
Alternatively, it is pretty easy to do runtime type checking by declaring a type of all possible values.
data Value
= VUnit -- of type One
| VPair Value Value -- of type Pair
| VFunc (Value -> Interp Value) -- of type Func
| VNat Integer -- of type Nat
Then you can very directly use your untyped THom, for an appropriate interpreter monad Interp (maybe just an Except monad):
eval :: THom -> Value -> Interp Value
eval Id v = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"
Notice also that VFunc above has the same type as the codomain of eval, since embedded functions may also fail.
answered Jan 2 at 2:41
luquiluqui
48k6114168
add a comment |
Alternatively, it is pretty easy to do runtime type checking by declaring a type of all possible values.
data Value
= VUnit -- of type One
| VPair Value Value -- of type Pair
| VFunc (Value -> Interp Value) -- of type Func
| VNat Integer -- of type Nat
Then you can very directly use your untyped THom, for an appropriate interpreter monad Interp (maybe just an Except monad):
eval :: THom -> Value -> Interp Value
eval Id v = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"
Notice also that VFunc above has the same type as the codomain of eval, since embedded functions may also fail.
answered Jan 2 at 2:41
luquiluqui
48k6114168
Alternatively, it is pretty easy to do runtime type checking by declaring a type of all possible values.
data Value
= VUnit -- of type One
| VPair Value Value -- of type Pair
| VFunc (Value -> Interp Value) -- of type Func
| VNat Integer -- of type Nat
Then you can very directly use your untyped THom, for an appropriate interpreter monad Interp (maybe just an Except monad):
eval :: THom -> Value -> Interp Value
eval Id v = v
eval Unit _ = VUnit
eval Zero VUnit = VNat Zero
eval Succ (VNat n) = VNat (n + 1)
...
eval _ _ = throwE "type error"
Notice also that VFunc above has the same type as the codomain of eval, since embedded functions may also fail.
answered Jan 2 at 2:41
luquiluqui
48k6114168
answered Jan 2 at 2:41
luquiluqui
48k6114168
answered Jan 2 at 2:41
luquiluqui
48k6114168
answered Jan 2 at 2:41
luquiluqui
48k6114168
48k6114168
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53996638%2fhaskell-interpreter-for-system-t-combinator-language%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
In your previous question, you say that you want to "use this for an external language". Can you elaborate? Would a printer of
THomterms to your target language answer your question (in which case a description of said language seems necessary)?– Li-yao Xia
Jan 1 at 17:41
You can compute with values in some type that can encode all the possible values. That way you can do runtime type checking.
– augustss
Jan 2 at 0:19
@augustss please expand into an answer.
– CMCDragonkai
Jan 2 at 1:58
I’ll expand my answer when I’m not on my phone.
– augustss
Jan 2 at 9:15