On Wed, Feb 25, 2015 at 2:45 AM, Keean Schupke <[email protected]> wrote: > On 25 February 2015 at 07:37, Matt Oliveri <[email protected]> wrote: >> >> On Wed, Feb 25, 2015 at 2:02 AM, Keean Schupke <[email protected]> wrote: >> > 2) I still don't understand why you think these other methods of >> > specialisation are not useable when you have a subtyping relationship in >> > the >> > type system? >> >> The reason my proposal doesn't use subtyping is not because I think >> subtyping is not flexible enough. It's because I think it's too >> flexible! It allows things that I don't see how to implement without >> implicit allocations. Please don't ask me to repeat the example that >> we discussed all day. > > Hmm, I don't see any examples that I don't think work, so I can only assume > you see the implementation working differently. Those coercion functions you > posted would never be implicitly used, and the typing would not allow them > implicitly, but it would allow them to be explicitly defined.
Feast your eyes on this long-forgotten discussion from yesterday: ==-- On Tue, Feb 24, 2015 at 10:07 AM, Matt Oliveri <[email protected]> wrote: > On Tue, Feb 24, 2015 at 9:39 AM, Keean Schupke <[email protected]> wrote: >> Can you give me an example where you think the subtyping admits a type that >> arity-abstract types do not? If you believe there is a difference, you >> should be able to provide an example. > > You mean admits a program? That's very easy. The basic problem with > subtyping that it admits coercions: > > upcast1_1to2 (f : fn 1 a->fn 1 b->c) : fn 2 a->b->c = f > > This function allocates. ==-- On Tue, Feb 24, 2015 at 12:05 PM, Matt Oliveri <[email protected]> wrote: > On Tue, Feb 24, 2015 at 11:58 AM, Keean Schupke <[email protected]> wrote: >> upcast1_1to2 (f : fn 1 a->fn 1 b->c) : fn 2 a->b->c = f >> >> first I don't understand this type, do you mean >> >> cast1 :: fn 1 (fn 2 'a -> 'b -> 'c) -> (fn 1 'a -> fn 1 'b -> 'c) >> >> or >> >> cast2 :: fn 1 (fn 1 'a -> fn 1 'b -> 'c) -> (fn 2 'a -> 'b -> 'c) > > Ah, sorry. That was OCaml notation, which I prefer. In Haskell it'd be > like cast2. (Except actually OCaml would have quotes, and Haskell > wouldn't, I thought.) ==-- On Tue, Feb 24, 2015 at 10:24 AM, Matt Oliveri <[email protected]> wrote: > On Tue, Feb 24, 2015 at 10:18 AM, Keean Schupke <[email protected]> wrote: >> On 24 February 2015 at 15:07, Matt Oliveri <[email protected]> wrote: >>> upcast1_1to2 (f : fn 1 a->fn 1 b->c) : fn 2 a->b->c = f >> >> Hmm but this coercion is safe, as all we are doing is this: >> >> upcast1_1to2 f x y = (f x) y > > No, because in BitC, that would require f, x , and y to be passed at > once. You'd have to write it with a lambda. ==-- I don't know if you think that issue has been resolved, but in my mind, it hasn't. You still haven't given a correct account of how upcast1_1to2 gets implemented. (You may have noticed that I also challenged Shap to implement it.) > I'll post an implementation in logic when I have it working, and that should > explain how it works much more clearly. This implementation is just the type checker, right? That's not what I'm concerned about if it's true that you're just using unrestricted subtyping among arity-concrete function types. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
