Wow, Jeremy, your solution looks very nice. I'll try it and report back<div>Thanks a lot!!<br><br><div class="gmail_quote">2012/5/3 Jeremy Shaw <span dir="ltr"><<a href="mailto:jeremy@n-heptane.com" target="_blank">jeremy@n-heptane.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This response is written in literal Haskell.<br>
<br>
> {-# LANGUAGE DataKinds, KindSignatures, GADTs #-}<br>
<br>
The key to getting the type checker involved is to put the information<br>
where the type-checker can see it -- namely, the type signature.<br>
<br>
So, let's change A so that the Safe/Unsafe information is in the type:<br>
<br>
> data A safety = A Int<br>
<br>
This is what is called a 'phantom type', because the 'safety' type<br>
variable only appears on the left hand side. We can keep 'B' the same:<br>
<div class="im"><br>
> data B = B Int<br>
<br>
</div>Now, we need some way to represent 'Safe' and 'Unsafe':<br>
<br>
> data Safe<br>
> data Unsafe<br>
<br>
Normally data declarations have 1 or more data constructors. Here we<br>
have data-types with 0 constructors. We don't need to actually create<br>
any 'Safe' or 'Unsafe' values, because we are only going to be using<br>
them as the phantom arguments. We need two separate types, because we<br>
want to be able to tell the difference at compile time. As you saw,<br>
having a single type with two different constructors does not give you<br>
enough power to constrain things at compile time.<br>
<br>
Now we can make two helper functions which mark a value as 'Safe' or 'Unsafe':<br>
<br>
> unsafe :: A safety -> A Unsafe<br>
> unsafe (A x) = (A x)<br>
<br>
> safe :: A safety -> A Safe<br>
> safe (A x) = (A x)<br>
<br>
And now we can make 'createB' only accept safe values:<br>
<br>
> createB :: A Safe -> B<br>
> createB (A x) = B x<br>
<br>
We can apply createB to 'Safe' values:<br>
<br>
> b :: B<br>
> b = createB (safe (A 1))<br>
<br>
but not 'Unsafe' values:<br>
<br>
> {-<br>
<br>
> b2 :: B<br>
> b2 = createB (unsafe (A 1))<br>
<br>
Results in:<br>
<br>
Couldn't match expected type `Safe' with actual type `Unsafe'<br>
Expected type: A Safe<br>
Actual type: A Unsafe<br>
<br>
> -}<br>
<br>
Alas, we can also apply 'createB' to values that are untagged:<br>
<br>
> b3 :: B<br>
> b3 = createB (A 1)<br>
<br>
Sometimes that is a good thing -- but in this case, it is not likely<br>
to be. A work around is to not export the 'A' constructor. Instead we<br>
could export:<br>
<br>
> unsafeA :: Int -> A Unsafe<br>
> unsafeA x = (A x)<br>
<br>
> safeA :: Int -> A Safe<br>
> safeA x = (A x)<br>
<br>
If that is the only way to create values of type 'A', then we won't<br>
have any untagged 'A' values.<br>
<br>
With our current definition for 'A' we can mark values as 'Safe' or<br>
'Unsafe' and prevent functions from being applied at compile time.<br>
However, this provides no easy way to write a function that behaves<br>
one way for 'Safe' values and a different way for 'Unsafe' values. If<br>
we wanted to do that, we would need to create a type class.<br>
<br>
We might try to fix this by changing A to have two constructors again:<br>
<br>
] data A' safety = SafeA' Int | UnsafeA' Int<br>
<br>
But, now we have a very difficult problem of ensuring that values<br>
which use SafeA' always have the phantom type 'Safe' and that UnsafeA'<br>
values always have the phantom type 'Unsafe'. That is rather tricky.<br>
<br>
The solution here is the GADTs type extension. We can instead write:<br>
<br>
> data A' safety where<br>
> UnsafeInt :: Int -> A' Unsafe<br>
> SafeInt :: Int -> A' Safe<br>
<br>
This declaration is similar to the normal data declaration:<br>
<br>
] data A' safety<br>
] = UnsafeInt Int<br>
] | SafeInt Int<br>
<br>
But in the GADT version, we can specify that when we use the<br>
'UnsafeInt' constructor the phantom type variable *must* be 'Unsafe'<br>
and when using 'SafeInt' the phantom parameter *must* be 'Safe'.<br>
<br>
This solves both 'issues' that we described. We can now match on safe<br>
vs unsafe construtors *and* we can be sure that values of type A' are<br>
*always* marked as 'Safe' or 'Unsafe'. If we wanted to have an<br>
untagged version we could explicitly add a third constructor:<br>
<br>
> UnknownInt :: Int -> A' safety<br>
<br>
<br>
We can now write 'createB' as:<br>
<br>
> createB' :: A' Safe -> B<br>
> createB' (SafeInt i) = B i<br>
<br>
In this case createB' is total. The compiler knows that createB' could<br>
never be called with 'UnsafeInt' value. In fact, if you added:<br>
<br>
] createB' (UnsafeInt i) = B i<br>
<br>
you would get the error:<br>
<br>
Couldn't match type `Safe' with `Unsafe'<br>
Inaccessible code in<br>
a pattern with constructor<br>
UnsafeInt :: Int -> A' Unsafe,<br>
<br>
One issue with both A and A' is that the phantom variable parameter<br>
can be any type at all. For example we could write:<br>
<br>
> nonsense :: A' Char<br>
> nonsense = UnknownInt 1<br>
<br>
But, the only types we want to support are 'Safe' and 'Unsafe'. A'<br>
Char is a legal -- but meaningless type.<br>
<br>
In GHC 7.4 we can use Datatype promotion to make the acceptable types<br>
for the phantom parameter more restrictive.<br>
<br>
First we declare a normal Haskell type with constructors for safe and unsafe:<br>
<br>
> data Safety = IsSafe | IsUnsafe<br>
<br>
But, with the 'DataKind' extension enabled, we can now use this type<br>
to provide a signature for the the phantom type. The data type<br>
'Safety' automatically becomes a kind type 'Safety' and the data<br>
constructors 'IsSafe' and 'IsUnsafe' automatically become type<br>
constructors. Now we can write:<br>
<br>
> data Alpha (safetype :: Safety) where<br>
> SafeThing :: Int -> Alpha IsSafe<br>
> UnsafeThing :: Int -> Alpha IsUnsafe<br>
> UnknownThing :: Int -> Alpha safetype<br>
<br>
Now we can write:<br>
<br>
> foo :: Alpha IsUnsafe<br>
> foo = UnknownThing 1<br>
<br>
But if we try;<br>
<br>
] foo' :: Alpha Char<br>
] foo' = UnknownThing 1<br>
<br>
we get the error:<br>
<br>
Kind mis-match<br>
The first argument of `Alpha' should have kind `Safety',<br>
but `Char' has kind `*'<br>
In the type signature for foo': foo' :: Alpha Char<br>
<br>
hope this helps!<br>
<span class="HOEnZb"><font color="#888888">- jeremy<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
On Thu, May 3, 2012 at 10:36 AM, Ismael Figueroa Palet<br>
<<a href="mailto:ifigueroap@gmail.com">ifigueroap@gmail.com</a>> wrote:<br>
> Hi, I'm writing a program like this:<br>
><br>
> data B = B Int<br>
> data A = Safe Int | Unsafe Int<br>
><br>
> createB :: A -> B<br>
> createB (Safe i) = B i<br>
> createB (Unsafe i) = error "This is not allowed"<br>
><br>
> Unfortunately, the situation when createB is called with an Unsafe value is<br>
> only checked at runtime.<br>
> If I omit the second case, it is not an error to not be exhaustive :-(<br>
><br>
> Is there a way to make it a compile time error??<br>
><br>
> Thanks!<br>
> --<br>
> Ismael<br>
><br>
><br>
</div></div><div class="HOEnZb"><div class="h5">> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br>Ismael<br><br>
</div>