Left-to-right bias in type checking GADT functions
Hi all, I have to admit that I haven't checked if this is a known issue... The following is tested with both GHC 6.4.1 and 6.4.2; I have not checked the HEAD. Let me define a simple GADT |F|, -- a simple GADT data F :: * -> * where F :: Int -> F () and a more or less trivial function |g| operating on it: -- type checks g :: F a -> a -> Int g (F n) () = n No problems up to here. But then let me just flip the parameters of | g|---and call the resulting function |h|: -- does not type check h :: a -> F a -> Int h () (F n) = n -- !!! Now, this definition of h does not type check: Couldn't match the rigid variable `a' against `()' `a' is bound by the type signature for `h' Expected type: a Inferred type: () When checking the pattern: () In the definition of `h': h () (F n) = n So, it seems that there's a left-to-right bias in type checking functions over GADTs. I cannot imagine this being by design, for it certainly seems possible to type check functions of this sort in a conceptually unbiased fashion. Anyone to shine a light on this? TIA, Stefan ------------------------------------------ Bias.lhs:
{-# OPTIONS -fglasgow-exts #-}
-- a simple GADT data F :: * -> * where F :: Int -> F ()
-- type checks g :: F a -> a -> Int g (F n) () = n
-- does not type check h :: a -> F a -> Int h () (F n) = n -- !!!
Yes, it's quite deliberate. See 5.4 of http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf The alternative design choice is to reject both programs, but in Haskell (because of laziness) the evaluation order is prescribed, so accepting the former seems right. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] | On Behalf Of Stefan Holdermans | Sent: 20 June 2006 08:53 | To: Glasgow Haskell Users | Subject: Left-to-right bias in type checking GADT functions | | Hi all, | | I have to admit that I haven't checked if this is a known issue... | The following is tested with both GHC 6.4.1 and 6.4.2; I have not | checked the HEAD. | | Let me define a simple GADT |F|, | | -- a simple GADT | data F :: * -> * where F :: Int -> F () | | and a more or less trivial function |g| operating on it: | | -- type checks | g :: F a -> a -> Int | g (F n) () = n | | No problems up to here. But then let me just flip the parameters of | | g|---and call the resulting function |h|: | | -- does not type check | h :: a -> F a -> Int | h () (F n) = n -- !!! | | Now, this definition of h does not type check: | | Couldn't match the rigid variable `a' against `()' | `a' is bound by the type signature for `h' | Expected type: a | Inferred type: () | When checking the pattern: () | In the definition of `h': h () (F n) = n | | So, it seems that there's a left-to-right bias in type checking | functions over GADTs. I cannot imagine this being by design, for it | certainly seems possible to type check functions of this sort in a | conceptually unbiased fashion. | | Anyone to shine a light on this? | | TIA, | | Stefan | | | ------------------------------------------ | | Bias.lhs: | | > {-# OPTIONS -fglasgow-exts #-} | | > -- a simple GADT | > data F :: * -> * where F :: Int -> F () | | > -- type checks | > g :: F a -> a -> Int | > g (F n) () = n | | > -- does not type check | > h :: a -> F a -> Int | > h () (F n) = n -- !!! | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon,
Yes, it's quite deliberate. See 5.4 of
http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf The alternative design choice is to reject both programs, but in Haskell (because of laziness) the evaluation order is prescribed, so accepting the former seems right.
Yes, I've read it now and your point is clear. Thank you. Regards, Stefan
participants (2)
-
Simon Peyton-Jones -
Stefan Holdermans