On 29 April 2015 at 04:18, Matt Oliveri <atma...@gmail.com> wrote: > On Tue, Apr 28, 2015 at 12:18 PM, William ML Leslie > <william.leslie....@gmail.com> wrote: > > 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), > > 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. >
So you've got something like class Baz v ... instance (Foo t) => Baz List t ... Then the function from `Baz List Bar` to the instance is not injective, because `Foo Bar` is determined contextually and may vary depending on where we asked for a Baz List Bar. > 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. > Yes, and it's great, and it's sound. What I am describing is how to ensure that the *implicitly* resolvable instances satisfy the diagram Edward drew. You would not have two instances for (Foo Bar) that you expect to get resolved implicitly in the same scope. You'd provide one of them explicitly. -- 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
