I don't know if this is what you want but I was at least able to make it
to type check basically changing (fz . return) into simply return. I
think the error message about the occurs check was because of the fz
function is used wrong (or you didn't give it a correct type).
{-# LANGUAGE NoMonomorphismRestriction,TypeSynonymInstances,FlexibleInstances,MultiParamTypeClasses,ScopedTypeVariables #-}
-- Haskell' Committee seems to have agreed to remove the restriction
-- Tagless Typed lambda-calculus with integers and the conditional
-- in the higher-order abstract syntax.
-- Haskell itself ensures the object terms are well-typed.
-- Here we use the tagless final approach.
{-
module EvalTaglessF where
class Symantics repr where
l :: (repr t1 -> repr t2) -> repr (t1->t2)
a :: repr (t1->t2) -> repr t1 -> repr t2
i :: Int -> repr Int
(+:) :: repr Int -> repr Int -> repr Int -- addition
ifz :: repr Int -> repr t -> repr t -> repr t -- if zero
fix :: repr ((a->b) -> (a->b)) -> repr (a->b)
-- Let :: repr t1 -> (repr t1 -> repr t) -> repr t
-- compared to EvalTaglessI, everything is in lower-case now
-- Since we rely on the metalanguage for typechecking and hence
-- type generalization, we have to use `let' of the metalanguage.
infixl 9 `a`
-- It is quite challenging to show terms. Yet, in contrast to the GADT-based
-- approach (EvalTaglessI.hs), we are able to do that, without
-- extending our language with auxiliary syntactic forms.
-- Incidentally, showing of terms is just another way of _evaluating_
-- them, to strings.
type VarCount = Int -- to build the names of variables
newtype S t = S (VarCount -> (String,VarCount))
evals (S t) = t
instance Symantics S where
l f = S $ \c0 ->
let vname = "v" ++ show c0
c1 = succ c0
(s,c2) = evals (f (S $ \c -> (vname,c))) c1
in ("(\\" ++ vname ++ "-> " ++ s ++ ")",c2)
a e1 e2 = S $ \c0 ->
let (s1,c1) = evals e1 c0
(s2,c2) = evals e2 c1
in ("(" ++ s1 ++ " " ++ s2 ++ ")",c2)
i n = S $ \c -> (show n,c)
e1 +:e2 = S $ \c0 ->
let (s1,c1) = evals e1 c0
(s2,c2) = evals e2 c1
in ("(" ++ s1 ++ " + " ++ s2 ++ ")",c2)
ifz e1 e2 e3 = S $ \c0 ->
let (s1,c1) = evals e1 c0
(s2,c2) = evals e2 c1
(s3,c3) = evals e3 c2
in ("(ifz " ++ s1 ++ " " ++ s2 ++ " " ++ s3 ++")",c3)
fix e = S $ \c0 ->
let (s1,c1) = evals e c0
in ("(fix " ++ s1 ++ ")",c1)
tshow t = fst $ evals t 0
-- We no longer need variables or the environment and we do
-- normalization by evaluation.
-- Denotational semantics. Why?
newtype D t = D t -- This is not a tag. Why?
evald:: D t -> t
evald (D t) = t
instance Symantics D where
l f = D $ \x -> evald (f (D x))
a e1 e2 = D $ (evald e1) (evald e2)
i n = D $ n
e1 +: e2 = D $ evald e1 + evald e2
ifz e1 e2 e3 = D $ if evald e1 == 0 then evald e2 else evald e3
fix e = D $ hfix (evald e) where hfix f = f (hfix f)
{-
We can also give operational semantics, by implementing the function of the
following signature:
evalo :: (forall repr. Symantics repr => repr t) ->
(forall repr. Symantics repr => repr t)
The signature has rank-2 type and hence this file requires a PRAGMA
declaration {-# LANGUAGE Rank2Types #-}
The implementation of evalo is exactly the partial evaluator of the
tagless final paper. Please see the paper for details.
-}
-- Tests
-- Truly the tests differ from those in EvalTaglessI.hs only in the case
-- of `syntax`: (i 1) vs (I 1), etc.
test0d = evald $ l(\vx -> vx +: (i 2)) `a` (i 1) -- 3
term1 = l (\vx -> ifz vx (i 1) (vx +: (i 2)))
test11d = evald $ term1
test11s = tshow $ term1 -- "(\\v0-> (ifz v0 1 (v0 + 2)))"
test12d = evald (term1 `a` (i 2)) -- 4, as Haskell Int
-- test14 = evald (term1 `a` vx) -- Type error! Not in scope: `vx'
term2 = l (\vx -> l (\vy -> vx +: vy))
-- *EvalTaglessF> :t term2
-- term2 :: (Symantics repr) => repr (Int -> Int -> Int)
test21 = evald term2
test23d = evald (term2 `a` (i 1) `a` (i 2)) -- 3
termid = l(\vx -> vx)
testid = evald termid -- testid :: t1 -> t1
term2a = l (\vx -> l(\vy -> vx `a` vy))
{- The meta-language figured the (polymorphic) type now
*EvalTaglessF> :t term2a
term2a :: (Symantics repr) => repr ((t1 -> t2) -> t1 -> t2)
-}
-- No longer hidden problems
-- term3 = l (\vx -> ifz vx (i 1) vy) -- Not in scope: `vy'
-- The following is a type error, we can't even enter the term
-- term4 = l (\vx -> ifz vx (i 1) (vx `a` (i 1)))
{- Now we get good error messages!
Couldn't match expected type `t1 -> Int'
against inferred type `Int'
Expected type: repr (t1 -> Int)
Inferred type: repr Int
In the first argument of `a', namely `vx'
In the third argument of `ifz', namely `(vx `a` (i 1))'
-}
-- (x+1)*y = x*y + y
-- why is this less of a cheating? Try showing the term
-- Now, both type-checking and evaluation of tmul1 works!
tmul1 = l (\vx -> l (\vy ->
(ifz vx (i 0)
((tmul1 `a` (vx +: (i (-1))) `a` vy) +: vy))))
-- tmul1 :: (Symantics repr) => repr (Int -> Int -> Int)
testm1d = evald (tmul1 `a` (i 2) `a` (i 3)) -- 6
-- Can termY be typechecked?
-- delta = l (\vy -> vy `a` vy)
{-
Occurs check: cannot construct the infinite type: t1 = t1 -> t2
Expected type: repr t1
Inferred type: repr (t1 -> t2)
In the second argument of `a', namely `vy'
In the expression: vy `a` vy
-}
tmul = fix (l (\self -> l (\vx -> l (\vy ->
(ifz vx (i 0)
((self `a` (vx +: (i (-1))) `a` vy) +: vy))))))
testm21d = evald tmul
testm23d = evald (tmul `a` (i 2) `a` (i 3)) -- 6
-- Tests of let (cf. the corresponding tests in TInfLetP.hs)
testl1 = let vx = vx in vx -- why this works in Haskell?
-- testl2 = let vx = vy in (i 1) -- type error
testl3 = evald $ let vx = i 1 in vx +: vx -- 2
-- this is essentially the test of hygiene
testl5 = evald $ l(\vx -> let vy = vx `a` (i 1) in l(\vx -> vy +: vx))
-- testl5 :: (Int -> Int) -> Int -> Int
-- lambda vs. let-bound variables
testl61 = evald $ l(\vx -> let vy = vx `a` (i 1) in
let vz = vy +: (i 2) in vy)
-- testl61 :: (Int -> Int) -> Int
testl62 = evald $ l(\vx -> let vy = vx `a` (i 1) in
let vz = vy +: (i 2) in vx)
-- testl62 :: (Int -> Int) -> Int -> Int
testl63 = evald $ l(\vx -> let vy = vx `a` (i 1) in
let vz = (i 2) in vx)
-- testl63 :: (Int -> t2) -> Int -> t2
testl71 = evald $ let vx = term2a in vx
-- testl71 :: (t1 -> t2) -> t1 -> t2
testl72 = evald $ let vx = term2a in
let vy = vx `a` termid in
let vz = vy `a` (i 2) in vx
-- testl72 :: (t1 -> t2) -> t1 -> t2
testl73 = evald $ let vx = term2a in
let vy = vx `a` termid in
let vz = vy `a` (i 2) in vy
-- testl73 :: t2 -> t2
testl74 = evald $ let vx = term2a in
let vy = let z = vx `a` tmul in vx `a` termid
in vy
-- testl74 :: t2 -> t2
testl75 = evald $ let vx = term2a in
let vy = let z = vx `a` termid in z
in vy
-- testl75 :: t2 -> t2
term2id = let id = l(\vx ->vx) in
l(\f -> l(\vy ->
((i 2) +:
((id `a` f) `a` ((id `a` vy) +: (i 1))))))
test2id = evald term2id
-- test2id :: (Int -> Int) -> Int -> Int
termlet = let c2 = l(\f -> l(\vx -> f `a` (f `a` vx))) in
let inc = l(\vx -> vx +: (i 1)) in
let compose = l(\f -> l(\g -> l(\vx -> f `a` (g `a` vx)))) in
let id = l(\vx -> vx) in
c2 `a` (compose `a` inc `a` inc) `a` (i 10) +:
((c2 `a` (compose `a` inc) `a` id) `a` (i 100))
testlet = evald termlet -- 116
-}
import Control.Monad.State
type VarCount = Int
newtype Y b a = Y {unY :: VarCount -> (b, VarCount)}
newtype Z a b = Z {unZ :: Y b a}
instance Monad (Z a) where
return x = Z $ Y $ \c -> (x,c)
(Z (Y m)) >>= f = Z $ Y $ \c0 -> let (x,c1) = m c0 in (unY . unZ) (f x) c1 -- Pace, too-strict puritans
instance MonadState String (Z a) where
get = Z $ Y $ \c -> (show c, c)
put x = Z $ Y $ \_ -> ((), read x)
class Symantics repr where
int :: Int -> repr Int -- int literal
add :: repr Int -> repr Int -> repr Int
lam :: (repr a -> repr b) -> repr (a->b)
instance Symantics (Y String) where
int = unZ . return . show
add x y = unZ $ do
sx <- Z x
sy <- Z y
return $ "(" ++ sx ++ " + " ++ sy ++ ")"
lam = lam'
lam' :: forall a b . (Y String a -> Y String b) -> Y String (a->b)
lam' f = unZ $ do
show_c0 <- get
let
vname = "v" ++ show_c0
c0 = read show_c0 :: VarCount
c1 = succ c0
fz :: Z a String -> Z b String
fz = Z . f . unZ
put (show c1)
s <- return vname
return $ "(\\" ++ vname ++ " -> " ++ s ++ ")"
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
