Tail function for "safe list" using GADTs

Question

I was reading through a GADT walkthrough and got stuck on one of the exercises. The given data structure is:

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

The exercise is to implement a safeTail function. I'd like it to act similar to the tail function in Prelude:

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

^{(I didn't actually define ==, but hopefully it's clear what I mean)}

Can this be done? I'm not entirely sure what the type would even be... maybe safeTail :: MarkedList a Safe -> MarkedList a NotSafe?

Answer 1

It is possible to implement safeTail if you change the type structure a bit:

{-# 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

The problem with the original safeTail :: MarkedList a Safe -> MarkedList a b is that b can be any type - not necessarily the same type that the tail of the list is marked with. This is fixed here by reflecting the list structure on the type level which allows the return type of safeTail to be appropriately constrained.

Answer 2

Yes, it can be done. The trick is to turn that existentially-quantified contained list into a list of a known type: specifically, a NotSafe one!

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

Now we can take the tail safely:

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

Additionally, this pattern match is complete. You won't get a warning from -fwarn-incomplete-patterns, and if you try to add a Nil clause you'll get an error. Let's turn on StandaloneDeriving, derive a Show instance, and test out your samples:

*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