On 28 April 2015 at 20:43, Matt Oliveri <atma...@gmail.com> wrote: > On Tue, Apr 28, 2015 at 12:27 AM, William ML Leslie > <william.leslie....@gmail.com> wrote: > > 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. >
​Right, so sometimes you declare an instance for a type with no free variables. An instance for Int, an instance for List Int, those are not functions. But you can also declare an instance for (Foo 'a => List 'a). This type is a function (because 'a is free), and it is problematic because two instances for the single type List Bar may have inferred different instances for Foo Bar. That is, we searched for our List 'a, and got something with some extra hidden information. -- 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 bitc-dev@coyotos.org http://www.coyotos.org/mailman/listinfo/bitc-dev
