This program compiles and runs correctly under GHC:
type Church a = (a -> a) -> a -> a
ch :: Int -> Church a
ch 0 _ = id
ch n f = f . ch (n-1) f
unch :: Church Int -> Int
unch n = n (+1) 0
suc :: Church a -> Church a
suc n f = f . n f
pre :: Church ((a -> a) -> a) -> Church a
pre n f a = n s z id
where s g h = h (g f)
z = const a
main :: IO ()
main = do let seven = ch 7
eight = suc seven
six = pre seven
print (unch eight)
print (unch six)
But when compiling with Frege I got the following error:
E /home/xgp/work/flab/src/main/frege/flab/fold.fr:23: type error in expression seven
type is : Int
expected: (t1→t1)→t1
E /home/xgp/work/flab/src/main/frege/flab/fold.fr:23: type error in expression seven
type is : (t1→t1)→t1
expected: Int
E /home/xgp/work/flab/src/main/frege/flab/fold.fr:23: type error in expression seven
type is : (t1→t1)→t1
expected: Int
E /home/xgp/work/flab/src/main/frege/flab/fold.fr:23: type error in
expression seven
type is apparently Int
used as function
Why? Is it possible to modify the program to pass the compilation under Frege?