Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Tail function for "safe list" using GADTs

Tags:

haskell

gadt

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?

like image 619
Snowball Avatar asked Oct 31 '13 05:10

Snowball


2 Answers

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.

like image 95
Mikhail Glushenkov Avatar answered Nov 02 '22 23:11

Mikhail Glushenkov


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
like image 24
Daniel Wagner Avatar answered Nov 03 '22 00:11

Daniel Wagner