I think Keean linked me to this video some time ago, and I think I'm starting to get an understanding of what he is talking about. This is Edward Kmett's "Typeclasses vs The World".
https://www.youtube.com/watch?v=hIZxTQP1ifo My suspicion is that for implicits to satisfy commutativity of the diagram in this talk, typeclass parameters must be injective. This is a vastly simpler property to ensure if the type language is pure and total (as it is in bitc). It would be an interesting experiment to prove that. Also, the objections related to kind classes and associated types are clearly not injective. It's interesting that (real) type classes permit this and yet are coherent. The reason, evidently, is that associated types are never used for instance resolution. If all of this turns out to be true, we can probably get by requiring that types used to automatically infer the instance are injective. This is the direction Idris has moved in lately, so maybe there's proof somewhere that this is sufficient. -- 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
