Existential types: want better syntactic support (autoboxing?)

[John Meacham]

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⑈