On 2 January 2015 at 10:21, Geoffrey Irving <[email protected]> wrote: > On Thursday, January 1, 2015, Keean Schupke <[email protected]> wrote: >> How would you deal with existential types though? If instances can have >> different types, they can leak type information out of the existential >> container, which seems like it would be unsound. > > > I'm imagining that the implementation is the same as the fully dependently > typed version with implicits, namely dictionary passing.
Key to note that there is nothing particularly dependant about the way this works in Idris or Agda. In order to call a method that depends on a typeclass, you must have the instance. Whether this is passed as a type-level argument which gets inferred statically or passed as a dictionary at run-time it doesn't matter too much except that all variables that appear in the signature must be bound. Truly, Idris rots the brain. Even those aspects of it that are not exceedingly straightforward hint at how it should be done, make you wonder why you didn't think of this yourself, and make you ask why other languages did it differently. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
