haskell - GADT を使用した「セーフ リスト」のテール関数

Question

GADT ウォークスルーを読んでいて、演習の 1 つに行き詰まってしまいました。指定されたデータ構造は次のとおりです。

{-# 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適切に制限できるようにする型レベルでリスト構造を反映することで、ここで修正されます。