5

我正在阅读GADT 演练，但被困在其中一个练习上。给定的数据结构是：

{-# LANGUAGE GADTs, EmptyDataDecls, KindSignatures #-}
data NotSafe
data Safe
data MarkedList :: * -> * -> * where
    Nil  :: MarkedList t NotSafe
    Cons :: a -> MarkedList a b -> MarkedList a c

练习是实现一个safeTail功能。我希望它的行为类似于tailPrelude 中的功能：

safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil))) == Cons 'a' (Cons 't' Nil)
safeTail (Cons 'x' Nil)                       == Nil
safeTail Nil  -- type error (not runtime!)

（我实际上并没有定义==，但希望我的意思很清楚）

这可以做到吗？我不完全确定它会是什么类型……也许safeTail :: MarkedList a Safe -> MarkedList a NotSafe吧？

4

2 回答 2

7

safeTail如果您稍微更改类型结构，则可以实现：

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

data Safe a
data NotSafe

data MarkedList :: * -> * -> * where
    Nil  :: MarkedList t NotSafe
    Cons :: a -> MarkedList a b -> MarkedList a (Safe b)

safeHead :: MarkedList a (Safe b) -> a
safeHead (Cons h _) = h

safeTail :: MarkedList a (Safe b) -> MarkedList a b
safeTail (Cons _ t) = t

原始的问题safeTail :: MarkedList a Safe -> MarkedList a b是它b可以是任何类型 - 不一定与列表尾部标记的类型相同。这通过在类型级别上反映列表结构来解决此问题，这允许safeTail适当地约束的返回类型。

于 2013-10-31T05:40:20.300 回答
4

是的，这是可以做到的。诀窍是将存在量化的包含列表转换为已知类型的列表：具体来说，NotSafe一个！

unsafe :: MarkedList a b -> MarkedList a NotSafe
unsafe Nil = Nil
unsafe (Cons a b) = Cons a b

现在我们可以安全地抓住尾巴了：

safeTail :: MarkedList a Safe -> MarkedList a NotSafe
safeTail (Cons a b) = unsafe b

此外，此模式匹配已完成。您不会收到来自 的警告-fwarn-incomplete-patterns，如果您尝试添加Nil子句，则会收到错误消息。让我们打开StandaloneDeriving，派生一个Show实例，然后测试您的样本：

*Main> safeTail (Cons 'c' (Cons 'a' (Cons 't' Nil)))
Cons 'a' (Cons 't' Nil)
*Main> safeTail (Cons 'x' Nil)
Nil
*Main> safeTail Nil

<interactive>:10:10:
    Couldn't match type `NotSafe' with `Safe'
    Expected type: MarkedList a0 Safe
      Actual type: MarkedList a0 NotSafe
    In the first argument of `safeTail', namely `Nil'
    In the expression: safeTail Nil
    In an equation for `it': it = safeTail Nil
于 2013-10-31T07:27:06.830 回答