Re: [Haskell-cafe] Specify compile error

Wow, Jeremy, your solution looks very nice. I'll try it and report back Thanks a lot!! 2012/5/3 Jeremy Shaw

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Ismael