On Tue, Jan 31, 2006 at 02:26:02AM +0000, Philippa Cowderoy wrote:
On Mon, 30 Jan 2006, John Meacham wrote:
an alternative might be to just allow existential types in structures so we can have [exists a . Foo a => a], but that probably has its own can of worms...
Yup. The boxy types paper gives us impredicativity and allows us to define the type, but in GHC you can't allow [exists a . num a => a] to subsume [Int] because that'd require mapping across the list to add in the dictionaries. You can hack it for lists, but you can't do it for general structures.
I believe JHC could handle it fine though.
well, jhc would also need to pass a type parameter rather than a dictionary in so it would likely have a similar issue. although, that raises another good point about autoboxing, [Foo] and [Int] would necessarily be different types. so how would you convert [Int] to [Foo]? (map id)? yeah, I am more convinced that the proposal is good except for the autoboxing bit, we will have to introduce some sort of explicit boxing operation, but the type of said operator would be quite odd.. if we make the requirement it be called monomorphically in 'c' then it becomes simpler, but still.. it is very warty.. introducing a dataconstructor for each class might be the only way to go. box :: forall (c::class) (a::*) . c a => a -> (c::*) notice the wacky made up quantification over classes, and the fact that (c::*) and (c::class) are not the same, but are linked... not very good. John -- John Meacham - ⑆repetae.net⑆john⑈