On Tue, Apr 28, 2015 at 12:27 AM, William ML Leslie <[email protected]> wrote: > 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
Good video! I'm finally starting to get what the fuss over type classes is all about. > 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. I don't know what you mean. I know what an injective function is, but typeclass parameters are not necessarily functions. > 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. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
