frege - 弗雷格下的教会数字程序

Question

该程序在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)

但是在使用 Frege 编译时出现以下错误:

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

为什么？是否可以修改程序以通过弗雷格下的编译？

Answer 1

这是让绑定(bind)变量类型的泛化确实产生影响的罕见情况之一。

关键是，弗雷格的行为就像带有编译指示的 GHC -XMonoLocalBinds在这方面，有关详细信息，请参见此处:https://github.com/Frege/frege/wiki/GHC-Language-Options-vs.-Frege#Let-Generalization在这里:https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/other-type-extensions.html#typing-binds (还有一个指向 SPJ 论文的链接，它解释了基本原理)

简而言之，这意味着所有未注释的 let 绑定(bind)的 veriabes 都将具有单态类型，并且不能用于不同的类型。要恢复多态性，需要显式类型签名。

为了让你的程序能够编译，注解 seven 的绑定(bind)就足够了。和

seven :: Church a

关于 print/println:前者不刷新输出。所以你在 REPL 中有:

frege> print 'a'
IO ()
frege> print 'b'
IO ()
frege> println "dammit!"
abdammit!
IO ()