Wow, Jeremy, your solution looks very nice. I'll try it and report back Thanks a lot!!
2012/5/3 Jeremy Shaw <[email protected]> > 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 > <[email protected]> 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 > > [email protected] > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > -- Ismael
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
