[Haskell-cafe] Specify compile error
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
Re: [Haskell-cafe] Specify compile error
Nope - because at compile time, there's no way to know whether createB's argument is a Safe or an Unsafe. That information only exists at run time. Consider the following functions. f :: Int - A f x = if x 0 then Unsafe x else Safe x g :: IO B g = do x - getLine return $ createB $ f (read x) Here, read x will convert the input (entered at runtime) to an Int (assuming it can - failure leads to a runtime exception), and then f will convert the resulting Int to an A, which is then passed to createB. But there's no way of the compiler knowing whether that A will be a Safe or an Unsafe A, since that depends on the value entered at runtime. If you want the compiler to typecheck two things differently, they need to be of different types. If you give a bit more context about what you're trying to do, someone might be able to suggest a safer way of doing what it. Cheers, Adam On 3 May 2012 11:36, Ismael Figueroa Palet ifiguer...@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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Specify compile error
On Thu, May 3, 2012 at 5:36 PM, Ismael Figueroa Palet ifiguer...@gmail.comwrote: 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 :-( It is a warning at least, if you use the appropriate -W flag, or -Wall. You can combine it with -Werror to make it a compile-time error to omit cases in a pattern match (and other warnings.) I'm not quite sure what your intention with the A data type is. createB could also have the signature A - Maybe B, so the caller might check the outcome instead of having the entire program crash. Cheers, Aleks ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Specify compile error
Is there a way to make it a compile time error?? http://en.wikibooks.org/wiki/Haskell/GADT It may pay off talking about your specific use case. Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Specify compile error
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
safeAx = (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' =
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 jer...@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
safeAx = (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
