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?
This is one of those rare cases where generalization of types of let bound variables actually does make a difference.
The point is, Frege acts like GHC with pragma -XMonoLocalBinds in that respect, for details see here: https://github.com/Frege/frege/wiki/GHC-Language-Options-vs.-Frege#Let-Generalization and here: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/other-type-extensions.html#typing-binds (there is also a link to a paper of SPJ, that explains the rationale)
What this means, in short, is that all unannotated let bound veriabes will have a monomorphic type, and cannot be used at different types. To restore polymorphism, an explicit type signature is needed.
To make your program compile, it is enough to annotate the binding of seven with
seven :: Church a
Regarding print/println: the former one does not flush the output. So you have in the REPL:
frege> print 'a'
IO ()
frege> print 'b'
IO ()
frege> println "dammit!"
abdammit!
IO ()