[Haskell-cafe] Specify compile error

Jeremy Shaw jeremy at n-heptane.com
Thu May 3 20:57:55 CEST 2012


This response is written in literal Haskell.

> {-# LANGUAGE DataKinds, KindSignatures, GADTs #-}

The key to getting the type checker involved is to put the information
where the type-checker can see it -- namely, the type signature.

So, let's change A so that the Safe/Unsafe information is in the type:

> data A safety = A Int

This is what is called a 'phantom type', because the 'safety' type
variable only appears on the left hand side. We can keep 'B' the same:

> data B        = B Int

Now, we need some way to represent 'Safe' and 'Unsafe':

> data Safe
> data Unsafe

Normally data declarations have 1 or more data constructors. Here we
have data-types with 0 constructors. We don't need to actually create
any 'Safe' or 'Unsafe' values, because we are only going to be using
them as the phantom arguments. We need two separate types, because we
want to be able to tell the difference at compile time. As you saw,
having a single type with two different constructors does not give you
enough power to constrain things at compile time.

Now we can make two helper functions which mark a value as 'Safe' or 'Unsafe':

> unsafe :: A safety -> A Unsafe
> unsafe  (A x) = (A x)

> safe :: A safety -> A Safe
> safe    (A x) = (A x)

And now we can make 'createB' only accept safe values:

> createB :: A Safe -> B
> createB (A x) = B x

We can apply createB to 'Safe' values:

> b :: B
> b = createB (safe (A 1))

but not 'Unsafe' values:

> {-

> b2 :: B
> b2 = createB (unsafe (A 1))

Results in:

    Couldn't match expected type `Safe' with actual type `Unsafe'
    Expected type: A Safe
      Actual type: A Unsafe

> -}

Alas, we can also apply 'createB' to values that are untagged:

> b3 :: B
> b3 = createB (A 1)

Sometimes that is a good thing -- but in this case, it is not likely
to be. A work around is to not export the 'A' constructor. Instead we
could export:

> unsafeA :: Int -> A Unsafe
> unsafeA  x = (A x)

> safeA :: Int -> A Safe
> safeA    x = (A x)

If that is the only way to create values of type 'A', then we won't
have any untagged 'A' values.

With our current definition for 'A' we can mark values as 'Safe' or
'Unsafe' and prevent functions from being applied at compile time.
However, this provides no easy way to write a function that behaves
one way for 'Safe' values and a different way for 'Unsafe' values. If
we wanted to do that, we would need to create a type class.

We might try to fix this by changing A to have two constructors again:

] data A' safety = SafeA' Int | UnsafeA' Int

But, now we have a very difficult problem of ensuring that values
which use SafeA' always have the phantom type 'Safe' and that UnsafeA'
values always have the phantom type 'Unsafe'. That is rather tricky.

The solution here is the GADTs type extension. We can instead write:

> data A' safety where
>     UnsafeInt :: Int -> A' Unsafe
>     SafeInt   :: Int -> A' Safe

This declaration is similar to the normal data declaration:

] data A' safety
]     = UnsafeInt Int
]     | SafeInt Int

But in the GADT version, we can specify that when we use the
'UnsafeInt' constructor the phantom type variable *must* be 'Unsafe'
and when using 'SafeInt' the phantom parameter *must* be 'Safe'.

This solves both 'issues' that we described. We can now match on safe
vs unsafe construtors *and* we can be sure that values of type A' are
*always* marked as 'Safe' or 'Unsafe'. If we wanted to have an
untagged version we could explicitly add a third constructor:

>     UnknownInt   :: Int -> A' safety


We can now write 'createB' as:

> createB' :: A' Safe -> B
> createB' (SafeInt i) = B i

In this case createB' is total. The compiler knows that createB' could
never be called with 'UnsafeInt' value. In fact, if you added:

] createB' (UnsafeInt i) = B i

you would get the error:

    Couldn't match type `Safe' with `Unsafe'
    Inaccessible code in
      a pattern with constructor
        UnsafeInt :: Int -> A' Unsafe,

One issue with both A and A' is that the phantom variable parameter
can be any type at all. For example we could write:

> nonsense :: A' Char
> nonsense = UnknownInt 1

But, the only types we want to support are 'Safe' and 'Unsafe'. A'
Char is a legal -- but meaningless type.

In GHC 7.4 we can use Datatype promotion to make the acceptable types
for the phantom parameter more restrictive.

First we declare a normal Haskell type with constructors for safe and unsafe:

> data Safety = IsSafe | IsUnsafe

But, with the 'DataKind' extension enabled, we can now use this type
to provide a signature for the the phantom type. The data type
'Safety' automatically becomes a kind type 'Safety' and the data
constructors 'IsSafe' and 'IsUnsafe' automatically become type
constructors. Now we can write:

> data Alpha (safetype :: Safety) where
>     SafeThing    :: Int -> Alpha IsSafe
>     UnsafeThing  :: Int -> Alpha IsUnsafe
>     UnknownThing :: Int -> Alpha safetype

Now we can write:

> foo :: Alpha IsUnsafe
> foo  = UnknownThing 1

But if we try;

] foo' :: Alpha Char
] foo'  = UnknownThing 1

we get the error:

    Kind mis-match
    The first argument of `Alpha' should have kind `Safety',
    but `Char' has kind `*'
    In the type signature for foo': foo' :: Alpha Char

hope this helps!
- jeremy




On Thu, May 3, 2012 at 10:36 AM, Ismael Figueroa Palet
<ifigueroap at gmail.com> wrote:
> Hi, I'm writing a program like this:
>
> data B = B Int
> data A = Safe Int | Unsafe Int
>
> createB :: A -> B
> createB (Safe i) = B i
> createB (Unsafe i) = error "This is not allowed"
>
> Unfortunately, the situation when createB is called with an Unsafe value is
> only checked at runtime.
> If I omit the second case, it is not an error to not be exhaustive :-(
>
> Is there a way to make it a compile time error??
>
> Thanks!
> --
> Ismael
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>



More information about the Haskell-Cafe mailing list