On Tue, Apr 28, 2015 at 12:18 PM, William ML Leslie <[email protected]> wrote: > On 28 April 2015 at 20:43, Matt Oliveri <[email protected]> wrote: >> >> On Tue, Apr 28, 2015 at 12:27 AM, William ML Leslie >> <[email protected]> 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),
Are you talking about - some hypothetical function from instances of (Foo 'a) to instances of (List 'a) - the function from some type 'a to the constraint (Foo 'a => List 'a) or - the function from some type expression "'a" to the constraint expression "Foo 'a => List 'a" ? And you're saying it's not injective? I know the last one is injective. > 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. I don't understand. You could have two instances for (Foo Bar) sitting right next to each other with the instance arguments approach, I thought. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
