我一直在Haskell维基上阅读类型算术的页面,并且在类型系统中嵌入的lambda演算部分遇到了一些麻烦.从那一节,我收集到以下代码不适用于GHC/GHCi - 显然GHC不应该能够确定g的类型签名.
{-# OPTIONS -fglasgow-exts #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
data X
data App t u
data Lam t
class Subst s t u | s t -> u
instance Subst X u u
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')
instance Subst (Lam t) u (Lam t)
class Apply s t u | s t -> u
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'
class Eval t u | t -> u
instance Eval X X
instance Eval (Lam t) (Lam t)
instance (Eval s s', Apply s' t u) => Eval (App s t) u
f :: Eval (App (Lam X) X) u => u
f = undefined
g :: Eval (App (Lam (App X X )) (Lam (App X X ))) u => u
g = undefined
请注意,我必须添加FlexibleContexts和UndecidableInstances,因为给定的代码似乎没有这些扩展而编译.但是,当我使用GHCi(版本8.0.2)运行它时,我得到以下结果:
*Main> :t f
f :: X
*Main> :t g
g :: u
这对我来说特别奇怪,因为类型u没有在任何地方定义.这是上面两个语言扩展相互交互和glasgow-exts的结果吗？如果是这样,怎么样？
类型u只是一个单独的变量 - 就像ain undefined :: a.
要真正将其归结为其基本要素,请考虑以下备用文件:
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
class Loopy a
instance Loopy a => Loopy a
x :: Loopy a => a
x = undefined
如果你要求输入xghci 的类型,它会告诉你它有类型a,没有上下文.这看起来有点神奇; 你只需要意识到GHC中的实例解析完全被允许递归,并且实现很大程度上支持这一点.
如果您愿意,我们可以详细介绍您的示例中发生的情况,但它与上述文件非常类似.这是详细信息.
所以,我们想看看是否允许我们拥有此实例:
Eval (App (Lam (App X X)) (Lam (App X X))) u
我们知道
instance (Eval s s', Apply s' t u) => Eval (App s t) u
所以只要我们有这两个,我们就可以拥有它:
Eval (Lam (App X X)) s'
Apply s' (Lam (App X X)) u
第一个很容易,因为:
instance Eval (Lam t) (Lam t)
因此,当我们有以下情况时,我们可以获得蛋糕:
Apply (Lam (App X X)) (Lam (App X X)) u
以来
instance (Subst s t u, Eval u u') => Apply (Lam s) t u'
找到我们的蛋糕,我们应该检查下这两块石头:
Subst (App X X) (Lam (App X X)) u
Eval u u'
从
instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s' t')
我们知道我们什么时候可以吃蛋糕
Subst X (Lam (App X X)) s'
Subst X (Lam (App X X)) t'
Eval (App s' t') u'
这很容易取得进展,因为:
instance Subst X u u
因此,我们可以在以下情况下拥有原始实例:
Eval (App (Lam (App X X)) (Lam (App X X))) u'
但是,嘿presto!这是我们正在寻找的原始实例.总而言之,只要我们拥有原始实例,我们就可以拥有原始实例.所以我们声明我们可以拥有原始实例,然后我们可以拥有原始实例!不是那个桃子.