RE: GADT records revisited
It's a choice. Consider
data Bar a where
B1 :: { x :: b } - Bar [b]
B2 :: { x :: b } - Bar [b]
B3 :: Bar a
Now we can define a perfectly good selector
x :: Bar [b] - b
x (B1 v) = v
x (B2 v) = v
But this wouldn't work if the result types were different
data BadBar a where
B1 :: { x :: b } - Bar [b]
B2 :: { x :: b } - Bar b
B3 :: Bar a
Now it's true that in your example the field mentions only *polymorphic*
components, so there is a perfectly well-defined selector with the type you
give. Indeed, it could be a bit more complicated:
data FooBar x a where
Foo :: { fooBar :: a } - FooBar Char [a]
Bar :: { fooBar :: a } - FooBar Bool [a]
Then there is a reasonable selector with type
fooBar :: FooBar b [a] - a
So what is the general rule? When exactly is there a well-defined selector
type, and what is that type? Notice that in the type of fooBar we had to
generalise over the Char/Bool difference, but maintain the [a] part. Indeed it
might all be part of one type:
data FooBar2 x where
Foo2 :: { fooBar2 :: a } - FooBar2 (Char, [a])
Bar2 :: { fooBar2 :: a } - FooBar2 (Bool, [a])
So now
fooBar2 :: FooBar2 (x, [a]) - a
where we generalise part of the type.
So, on reflection, there must be a more permissive rule than the one GHC
currently implements. If someone wants to figure out the general rule, express
it formally, say what the user manual would say, we could discuss whether the
cost benefit ratio is good enough to be worth implementing.
This seems interesting enough to make into a ticket.
https://ghc.haskell.org/trac/ghc/ticket/8673
Simon
| -Original Message-
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Philip K.F. Hölzenspies
| Sent: 17 January 2014 06:51
| To: glasgow-haskell-users@haskell.org
| Subject: GADT records revisited
|
| Dear all,
|
| I was playing around with GADT-records again and ran into behaviour that
| I'm not sure is intentional. Given this program:
|
|
|
| {-#LANGUAGE GADTs #-}
|
| data FooBar x a where
|Foo :: { fooBar :: a } - FooBar Char a
|Bar :: { fooBar :: a } - FooBar Bool a
|
|
| GHC tells me this:
|
|
| foo.hs:3:1:
| Constructors Foo and Bar have a common field `fooBar',
|but have different result types
| In the data declaration for `FooBar'
| Failed, modules loaded: none.
|
|
| The user guide does say (section 7.4.7): However, for GADTs there is
| the following additional constraint: every constructor that has a field
| f must have the same result type (modulo alpha conversion). So this
| behaviour is documented in the user guide. However, it seems reasonable
| that in the case above, where all the relevant variables are exposed in
| the result type of both constructors, this should be perfectly typeable.
| In other words, shouldn't GHC be able to derive a type that is simply:
|
| fooBar :: FooBar x a - a
|
| ?
|
| Is this something that was simply never implemented, but could be, or is
| this not decidable or prohibitively computationally complex?
|
| Regards,
| Philip
|
|
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
GADT records revisited
Dear all,
I was playing around with GADT-records again and ran into behaviour that
I'm not sure is intentional. Given this program:
{-#LANGUAGE GADTs #-}
data FooBar x a where
Foo :: { fooBar :: a } - FooBar Char a
Bar :: { fooBar :: a } - FooBar Bool a
GHC tells me this:
foo.hs:3:1:
Constructors Foo and Bar have a common field `fooBar',
but have different result types
In the data declaration for `FooBar'
Failed, modules loaded: none.
The user guide does say (section 7.4.7): However, for GADTs there is
the following additional constraint: every constructor that has a field
f must have the same result type (modulo alpha conversion). So this
behaviour is documented in the user guide. However, it seems reasonable
that in the case above, where all the relevant variables are exposed in
the result type of both constructors, this should be perfectly typeable.
In other words, shouldn't GHC be able to derive a type that is simply:
fooBar :: FooBar x a - a
?
Is this something that was simply never implemented, but could be, or is
this not decidable or prohibitively computationally complex?
Regards,
Philip
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADT records revisited
I think this is intentional and conforms to the documentation. Your
constructors clearly have *different* result types, even though they
both can be instantiated from a single type scheme `FooBar x a`.
I'll leave it to others to comment on whether the generalization you
propose is reasonable and feasible.
Roman
* Philip K.F. Hölzenspies p.k.f.holzensp...@utwente.nl [2014-01-17
07:51:26+0100]
Dear all,
I was playing around with GADT-records again and ran into behaviour
that I'm not sure is intentional. Given this program:
{-#LANGUAGE GADTs #-}
data FooBar x a where
Foo :: { fooBar :: a } - FooBar Char a
Bar :: { fooBar :: a } - FooBar Bool a
GHC tells me this:
foo.hs:3:1:
Constructors Foo and Bar have a common field `fooBar',
but have different result types
In the data declaration for `FooBar'
Failed, modules loaded: none.
The user guide does say (section 7.4.7): However, for GADTs there is
the following additional constraint: every constructor that has a
field f must have the same result type (modulo alpha conversion). So
this behaviour is documented in the user guide. However, it seems
reasonable that in the case above, where all the relevant variables
are exposed in the result type of both constructors, this should be
perfectly typeable. In other words, shouldn't GHC be able to derive a
type that is simply:
fooBar :: FooBar x a - a
?
Is this something that was simply never implemented, but could be, or
is this not decidable or prohibitively computationally complex?
Regards,
Philip
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
signature.asc
Description: Digital signature
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
