GHC 7.8新语言特性: Roles

Roles用来解决GeneralizedNewtypeDeriving(GND)和其他语言扩展交互时导致类型系统不可靠的问题。

newtype和GND

Haskell的newtype可以在不引入运行时消耗的情况下构造新类型。

newtype Age = MkAge Int

Age类型在运行时就是一个Int，不需要额外的构造子，理想情况下这是一种没有消耗的抽象。

GND就是利用了newtype和底层表示的同构关系，自动派生出type class的实例。

class Inc a where
    inc :: a -> a

instance Inc Int where
    inc = (+1)

-- StandaloneDeriving
deriving instance Inc Age

newtype和GND都是很有用的特性，经常看到有人用这方法派生mtl里的各种类。

玩坏类型系统

这日子过的很好，直到遇上了GADT和type family。这两个扩展都有一个特点，就是根据类型做出不同选择。

例如年龄可以分为年轻和永远的17岁，数字可以分成1、2、⑨：

data AgeType = Young | Seventeen

data IntType = One | Two | Nine

我们自然可以把分类函数通过type class 重载：

class Classify a b where
    classify :: a -> b

这样可以吗？还不够，还要加上a、b间的函数依赖。函数依赖¹？为什么不用type family呢：

type family TypeOf a :: *
type instance TypeOf Int = IntType
type instance TypeOf Age = AgeType

class Classify a where
    classify :: a -> TypeOf a

instance Classify Int where
    classify 1 = One
    classify 2 = Two
    classify _ = Nine

deriving instance Classify Age

bad :: Int -> AgeType
bad = classify . MkAge

因为Age的Classify实例是从Int派生的，所实际上bad使用的是Int的Classify实例，bad就是把一个Age里的Int转成IntType，然后再转成AgeType。在生成的core里可以看到bad居然能把IntType直接类型强转成AgeType（因为被inline了，看不到字典传递）。

bad :: Int -> AgeType
bad =
  \ (x :: Int) ->
    case x of _ { I# ds ->
    case ds of _ {
      __DEFAULT -> Nine
        `cast` (Sym <(TFCo:R:TypeOfInt)> ;
		        (TypeOf (Sym <(NTCo:Age)>) ; <TFCo:R:TypeOfAge>)
                :: IntType ~# AgeType);
      1 -> One
        `cast` (Sym <(TFCo:R:TypeOfInt)> ;
		        (TypeOf (Sym <(NTCo:Age)>) ; <TFCo:R:TypeOfAge>)
                :: IntType ~# AgeType);
      2 -> Two
        `cast` (Sym <(TFCo:R:TypeOfInt)> ;
		        (TypeOf (Sym <(NTCo:Age)>) ; <TFCo:R:TypeOfAge>)
                :: IntType ~# AgeType)
    }
    }

类似的，利用GND和type family还能做出unsafeCoerce :: a -> b，总之就是把类型系统玩坏了。（GND还有其他问题，因为还没解决，就不先说了1）

为什么会这样？

从上面的例子可以看到，GND把Age和Int当作同一个类型，而type family又区分Age和Int，结果就是GND和type family混淆了运行时表示等价（representational equality）和类型等价（nominal equality），在不合适的地方重用了同一个type class实例，再进行了错误的强转。

落到实现上，newtype是通过在core里进行类型强转实现的。GND派生实例时直接了利用newtype不区分类型的运行表示的特点，重用了type class实例，然后type family、GADT又要求类型不同的结果，结果就是在core里把那个被重用的type class实例的结果强转到其他类型。

Roles

但是，我们能直接禁止GND和type Family的交互吗？GND用的好还是很方便的，所以应该区分什么时候是GND是可行的，什么时候是有害的。

观察发现，只要一个类型参数在type family、GADT和type class里不被检查（inspect）区分，不作为其他类型参数的参数，那么就可以重用这个类型参数的type class实例，最后的类型强转是安全的。这样的类型参数就充当representational的角色，表示newtype的实例和它的实例可以是相同的。

而对于其他被检查的类型参数，其newtype的实例应该是不同的，这样的类型参数充当nominal的角色，不同名字的类型要有不同的实例。

GeneralizedNewtypeDeriving works only with classes whose last type parameter is at role representational.

在上面的Inc类里，类型参数a没有被检查，inc直接就返回了同样类型的a，所以a是representational的，所以a的newtype可以重用a的type class实例。

在上面的TypeOf会根据a的不同返回不同的类型，所以这个a是nominal的。同理，Classify里的a也是nomimal的，所以a的newtype不能重用a的type class实例，应该禁止GND派生。

还有第三种role: phantom，主要用在phantom type，和消除某些情况下newtype转换的消耗（详见GHC7.8的Coercible）。

Role的推导由编译器完成，也可以手写注解，加强role的限制。

参考

1. GHC Wiki: Roles
2. Roles: a new feature of GHC
3. GeneralizedNewtypeDeriving is Profoundly Unsafe