Hello, I've been attempting to use GADTs to create a small domain specific language, and I'm running into an odd problem. Adding one case to the example at the beginning of the Wobbly types paper: data Term :: * -> * where Lit :: a -> Term a Inc :: Term Int -> Term Int IsZ :: Num a => Term a -> Term Bool Div :: Fractional a => Term a -> Term a -> Term a If :: Term Bool -> Term a -> Term a -> Term a and extending the eval function accordingly: eval :: Term a -> a eval (Lit i) = i eval (Inc t) = eval t + 1 eval (IsZ t) = eval t == 0 eval (Div t u) = eval t / eval u eval (If cond cons alt) = if eval cond then eval cons else eval alt I get an error "No instance for (Fractional a) arising from the use of '/'" This seems odd to me, since Div is constrained to have fractional arguments. Is there something obvious I'm missing? Thanks, /g
Hi Garrett,
I get an error "No instance for (Fractional a) arising from the use of '/'" This seems odd to me, since Div is constrained to have fractional arguments. Is there something obvious I'm missing?
Unless GADTs are handled specially, and I don't think they are in this case, this problem is not specific to GADTs but related to how type constraints on constructors are handled in general. Basically, a constraint on a constructor has no effect beyond beyond constraining what the constructor can be applied to (see the Haskell 98 report 4.2.1). In particular, when you take a constructed value apart through pattern matching, the constraints do not come into play: hence the "no instance" message. It has been suggested a number of times that constraints on constructors should have a more profound meaning, and maybe GADTs make this even more desirable, as your example suggest. Best regards, /Henrik -- Henrik Nilsson School of Computer Science and Information Technology The University of Nottingham nhn@cs.nott.ac.uk This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
I get an error "No instance for (Fractional a) arising from the use of '/'" This seems odd to me, since Div is constrained to have fractional arguments. Is there something obvious I'm missing?
Unless GADTs are handled specially, and I don't think they are in this case, this problem is not specific to GADTs but related to how type constraints on constructors are handled in general. Basically, a constraint on a constructor has no effect beyond beyond constraining what the constructor can be applied to (see the Haskell 98 report 4.2.1). In particular, when you take a constructed value apart through pattern matching, the constraints do not come into play: hence the "no instance" message.
I think this is the correct explanation. However, it might be confusing that IsZ :: Num a => Term a -> Term Bool and eval (IsZ t) = eval t == 0 works correctly. The difference here is that for IsZ, the compiler will store a Num dictionary within the constructed value, because a is existentially quantified. On the other hand, in Div :: Fractional a => Term a -> Term a -> Term a the a is visible on the outside, so the compiler does not store a dictionary. But then, while computing the pattern match eval (Div t u) = eval t / eval u there's really no way to create one. So, the question is, why cannot the compiler treat the case for Div more like the case for IsZ and store the Fractional dictionary within the constructor?
It has been suggested a number of times that constraints on constructors should have a more profound meaning, and maybe GADTs make this even more desirable, as your example suggest.
I think they do. Maybe the work that has already been done on GADTs and existentials finally make it possible to give an improved semantics to constraints on datatypes without too much additional work. Cheers, Andres
Henrik Nilsson
I get an error "No instance for (Fractional a) arising from the use of '/'" This seems odd to me, since Div is constrained to have fractional arguments. Is there something obvious I'm missing?
Unless GADTs are handled specially, and I don't think they are in this case, this problem is not specific to GADTs but related to how type constraints on constructors are handled in general. Basically, a constraint on a constructor has no effect beyond beyond constraining what the constructor can be applied to (see the Haskell 98 report 4.2.1). In particular, when you take a constructed value apart through pattern matching, the constraints do not come into play: hence the "no instance" message.
And in case anyone is wondering, you could fix the original program by adding the constraint to the function signature: eval :: Fractional a => Term a -> a although this is likely more constrained than the OP wanted. Regards, Malcolm
Hi Garret, As others have mentioned, this is currently not supported, but it seems that it will be at some point. On the sf bug-tracker, I could find the following entries, but the issue has also been discussed on the mailing list. http://sourceforge.net/tracker/index.php?func=detail&aid=1116210&group_id=8032&atid=108032 http://sourceforge.net/tracker/index.php?func=detail&aid=1180651&group_id=8032&atid=108032 Interestingly, unlike in the constrained-datatype-case, ghc's run-time representation of constrained gadts contains the dictionary, but there is no way to access it (well, except unsafeCoerce#) that I am aware of. So, how can we fake the desired behavior? Existential quantification allows us to store and access a dictionary, and we can witness type equality using GADTs, as in the E datatype below. Notice that Fractional b => f b can be expressed as exists a. (Fractional a) and (a = b) => f b Therefore, the following dataype is equivalent to yours and eval can be implemented on top of it. data E :: * -> * -> * where E :: E a a data Term :: * -> * where Lit :: a -> Term a Div :: Fractional a => E a b -> Term a -> Term a -> Term b eval :: Term a -> a eval (Lit i) = i eval (Div e t u) = let q = eval t / eval u in case e of E -> q The case for Div is a little awkward, as ghc needs to be forced to unify type variables and resolve constraints in a specific order for the trick to work. Regards, Thomas On Mon, 2005-10-10 at 13:06 -0400, J. Garrett Morris wrote:
I've been attempting to use GADTs to create a small domain specific language, and I'm running into an odd problem. Adding one case to the example at the beginning of the Wobbly types paper:
data Term :: * -> * where Lit :: a -> Term a Div :: Fractional a => Term a -> Term a -> Term a
and extending the eval function accordingly:
eval :: Term a -> a eval (Lit i) = i eval (Div t u) = eval t / eval u
participants (5)
-
Andres Loeh -
Henrik Nilsson -
J. Garrett Morris -
Malcolm Wallace -
Thomas Jäger