我可以完全禁用GHC上的类型检查,以便将其用作函数式语言的编译目标吗？

Question

GHC在这一点上的速度惊人地快.不过,我对Haskell的类型系统不满意,所以我决定将自己的系统作为DSL来实现.现在,我想通过翻译后检查无类型lambda演算表达式来编译我的语言到Haskell,以便使用GHC的性能.唯一的问题是我的系统上的某些有效表达式无法在GHC上编译.我怎样才能避免这个问题 - 即通过告诉GHC完全禁用类型系统"我已经检查了这个,相信我"？

Answer 1

你可以坚持unsafeCoerce每个子项目(或者,如果你有野心,只有实际需要的那些).

在评论中,您询问如何对此术语进行注释以使其进行类型检查:

div = (\ v0 -> (\ v1 -> (\ v2 -> (\ v3 -> ((v1 (\ v4 -> (v4 v3))) ((v0 (((v1 (\ v4 -> (\ v5 -> (\ v6 -> (v4 (\ v7 -> ((v5 v7) v6))))))) (\ v4 -> v4)) (\ v4 -> (\ v5 -> (v5 (v2 v4)))))) (((v1 (\ v4 -> (\ v5 -> v4))) (\ v4 -> v4)) (\ v4 -> v4))))))))

我跑进:s/(/unsafeCoerce (/g了vim,导致了这个术语:

div = unsafeCoerce (\ v0 -> unsafeCoerce (\ v1 -> unsafeCoerce (\ v2 -> unsafeCoerce (\ v3 -> unsafeCoerce (unsafeCoerce (v1 unsafeCoerce (\ v4 -> unsafeCoerce (v4 v3))) unsafeCoerce (unsafeCoerce (v0 unsafeCoerce (unsafeCoerce (unsafeCoerce (v1 unsafeCoerce (\ v4 -> unsafeCoerce (\ v5 -> unsafeCoerce (\ v6 -> unsafeCoerce (v4 unsafeCoerce (\ v7 -> unsafeCoerce (unsafeCoerce (v5 v7) v6))))))) unsafeCoerce (\ v4 -> v4)) unsafeCoerce (\ v4 -> unsafeCoerce (\ v5 -> unsafeCoerce (v5 unsafeCoerce (v2 v4)))))) unsafeCoerce (unsafeCoerce (unsafeCoerce (v1 unsafeCoerce (\ v4 -> unsafeCoerce (\ v5 -> v4))) unsafeCoerce (\ v4 -> v4)) unsafeCoerce (\ v4 -> v4))))))))

这加载了ghci,虽然我不知道它是否有效(或者即使我期望它).

编辑:经过一些检查,这可能不是一个公平/正确的方式来投入强制.(特别是,它会导致子类似v1 unsafeCoerce (\v4 -> ...)- 并且我们不应该在unsafeCoerce任何地方作为参数传递.)更正确的插入是unsafeCoerce在每个应用程序点插入一个,如下所示:

div = (\ v0 -> (\ v1 -> (\ v2 -> (\ v3 -> (unsafeCoerce (v1 (\ v4 -> (unsafeCoerce v4 v3))) (unsafeCoerce (v0 (unsafeCoerce (unsafeCoerce (unsafeCoerce v1 (\ v4 -> (\ v5 -> (\ v6 -> (unsafeCoerce v4 (\ v7 -> (unsafeCoerce (unsafeCoerce v5 v7) v6))))))) (\ v4 -> v4)) (\ v4 -> (\ v5 -> (unsafeCoerce v5 (unsafeCoerce v2 v4)))))) (unsafeCoerce (unsafeCoerce (unsafeCoerce v1 (\ v4 -> (\ v5 -> v4))) (\ v4 -> v4)) (\ v4 -> v4))))))))