利用类型系统表达约束

2012-05-04 黄毅

看邮件列表有一个回答很精彩,是一个很典型的利用类型系统表达约束的案例,故翻译过来。

原讨论:[http://article.gmane.org/gmane.comp.lang.haskell.cafe/98103]

问题:

我有一个这样的程序:

data B = B Int
data A = Safe Int | Unsafe Int

createB :: A -> B
createB (Safe i) = B i
createB (Unsafe i) = error "禁止出现"

问题是,使用 Unsafe 调用 createB 的情况只能在运行时才能检查,而如果去掉第二条分支,又变成了模式匹配不完备的错误了 :-(

有没有办法把它变成编译错误?

以下答复使用文学化Haskell(literate Haskell)写就。

{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

要让类型系统介入进来,关键在于把信息放在类型系统能看到的地方,也就是类型签名里面。

所以我们要把 A 类型改成这样,让 Safe/Unsafe 的信息出现在里面:

data A safety = A Int

这就是所谓的“phantom类型”了,因为 safety 类型变量只出现的类型定义的左边。B的类型可以保持不变:

data B        = B Int

现在,我们需要表达 "Safe" 和 "Unsafe":

data Safe
data Unsafe

通常数据类型定义会有一个或多个数据构造器。而这两个类型没有数据构造器,因为我们只打算把他们当作phantom类型参数用,不需要用到他们的值。我们需要两个独立的类型,是因为我们想在编译时区分两种情况。如果只定义一个类型带两个构造器的话,就没办法在编译时获得足够的约束能力了。

现在我们再定义两个函数把值标记成 Safe 或者 Unsafe:

unsafe :: A safety -> A Unsafe
unsafe  (A x) = (A x)

safe :: A safety -> A Safe
safe    (A x) = (A x)

然后我们把 createB 改成只接受 Safe 参数:

createB :: A Safe -> B
createB (A x) = B x

这样,我们就只能传给它 Safe 的参数:

b :: B
b = createB (safe (A 1))

而不能传 Unsafe 的参数:

{-

b2 :: B
b2 = createB (unsafe (A 1))

编译错误:

   Couldn't match expected type `Safe' with actual type `Unsafe'
   Expected type: A Safe
     Actual type: A Unsafe

-}

可惜,我们还是可以给 createB 传没标记过的值:

b3 :: B
b3 = createB (A 1)

有时候这是个好事,不过针对楼主的问题,应该是不想这种情况发生。有一个方案是不要导出 A 这个构造器,同时导出这样两个函数:

unsafeA :: Int -> A Unsafe
unsafeA  x = (A x)

safeA :: Int -> A Safe
safeA    x = (A x)

如果只能通过这两个函数创建类型 A 的值的话,那就不会存在没标记过的值了。

目前这个方案可以让我们把值标记成 Safe 或 Unsafe,并在编译时阻止某些函数的调用。 然而,要想写一个函数同时对两种情况进行处理却很麻烦,需要建个type class(译注:可以作为练习)。

不如还是把 A 改回成两个构造器的版本:

] data A' safety = SafeA' Int | UnsafeA' Int

现在,我们需要解决一个棘手的问题,就是如何保证 SafeA' 构造出来的值会带上phantom类型 Safe ,而 UnsafeA' 构造出来的值带phantom类型 Unsafe

要解决这个问题就要用 GADTs 类型扩展了,我们可以这么写:

data A' safety where
    UnsafeInt :: Int -> A' Unsafe
    SafeInt   :: Int -> A' Safe

这个定义和常规的数据类型定义很类似:

] data A' safety
]     = UnsafeInt Int
]     | SafeInt Int

但在 GADT 版本里面,我们可以指定当使用 UnsafeInt 的时候,phantom类型变量一定是 Unsafe ,而用 SafeInt 的时候一定是 Safe

这样就把上面说的两个问题都解决了,我们既可以对safe和unsafe两个构造器进行模式匹配,也可以保证 A' 类型一定会被标记成"Safe"或"Unsafe"。如果我们确实想要不标记的值,我们可以加一个构造器:

UnknownInt   :: Int -> A' safety

现在我们可以把 createB 改成这样了:

createB' :: A' Safe -> B
createB' (SafeInt i) = B i

这里, createB' 的定义是完备的,因为编译器知道它的参数不可能是 UnsafeInt 。如果你非要加上:

] createB' (UnsafeInt i) = B i

会得到编译错误:

Couldn't match type `Safe' with `Unsafe'
Inaccessible code in
  a pattern with constructor
    UnsafeInt :: Int -> A' Unsafe,

到现在, A and A' 两个版本都还存在的一个问题是,phantom类型变量可以是任何类型。比如我们可以这么写:

nonsense :: A' Char
nonsense = UnknownInt 1

我们只希望支持Safe和Unsafe,但 A' Char 也是一个合法——但是不合理的类型。

GHC 7.4 里面我们可以使用数据类型提升来约束phantom类型参数能接受的类型。

我们先定义一个普通的数据类型:

data Safety = IsSafe | IsUnsafe

只要启用了 DataKind 扩展,我们就可以把这个类型用作phantom类型参数的签名。这样,类型 Safety 会自动变成kind Safety ,而数据构造器 IsSafeIsUnsafe 自动变成类型构造器。现在我们就可以这么写:

data Alpha (safetype :: Safety) where
    SafeThing    :: Int -> Alpha IsSafe
    UnsafeThing  :: Int -> Alpha IsUnsafe
    UnknownThing :: Int -> Alpha safetype

然后,我们可以这么写:

foo :: Alpha IsUnsafe
foo  = UnknownThing 1

但是,如果我们尝试这么写的话:

] foo' :: Alpha Char
] foo'  = UnknownThing 1

就会得到一个编译错误:

Kind mis-match
The first argument of `Alpha' should have kind `Safety',
but `Char' has kind `*'
In the type signature for foo': foo' :: Alpha Char

希望这些能帮到你!


blog comments powered by Disqus

转载请注明出处,收藏或分享这篇文章到: