[Haskell-cafe] Specify compile error

[Ismael Figueroa Palet]

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

2012/5/3 Jeremy Shaw <jeremy at n-heptane.com>

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



-- 
Ismael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120503/058b864e/attachment.htm>