使用GADT的"安全列表"的尾部功能

Question

我正在阅读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？

Answer 1

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适当地约束返回类型.