Here's the implementation for functions of arity up to 2.
member(Key, cons(Head, Tail), Val) :-
dif(Key,Head),
member(Key, Tail, Val).
member(Key, cons(def(Key, Val), Tail), just(Val)).
member(Key, nil, nothing).
append(cons(H, T1), L, cons(H, T2)) :-
append(T1, L, T2).
append(nil, L, L).
subtype(fn(X, Y, Z), fn(X, fn(Y, Z))).
unify(X, X).
unify(X, Y) :-
subtype(X, Y).
unifyall(cons(T, Tail), T) :-
unifyall(Tail, T).
unifyall(nil, T).
unifyeach(cons(Tapp, Tail), Tdef, Cxt) :-
duplicate_term(Tdef, pair(C1, Tapp)),
unifyeach(Tail, Tdef, Csub),
append(Csub, C1, Cxt).
unifyeach(nil, Tdef, nil).
split(X, cons(def(Y, T), Tail1), Tail2, cons(def(Y, T), Tail3)) :-
dif(X, Y),
split(X, Tail1, Tail2, Tail3).
split(X, cons(def(X, T), Tail1), cons(T, Tail2), Tail3 ) :-
split(X, Tail1, Tail2, Tail3).
split(X, nil, nil, nil).
nat(zero).
nat(succ(X)) :-
nat(X).
bool(true).
bool(false).
expr(nat(X), nil, nat) :-
nat(X).
expr(bool(X), nil, bool) :-
bool(X).
expr(pair(X, Y), Cxt, prod(T1, T2)) :-
expr(X, C1, T1),
expr(Y, C2, T2),
append(C1, C2, Cxt).
expr(var(X), cons(def(X, Type), nil), Type).
expr(app(Fun, Arg), Cxt, B) :-
expr(Fun, C1, fn(A, B)),
expr(Arg, C2, A),
append(C1, C2, Cxt).
expr(app(F, A1, A2), C5, B) :-
expr(F, C1, TF),
expr(A1, C2, T1),
expr(A2, C3, T2),
unify(fn(T1, T2, B), TF),
append(C1, C2, C4),
append(C4, C3, C5).
expr(lam(Var, Body), Cxt, fn(A, B)) :-
expr(Body, C1, B),
split(Var, C1, Def, Cxt),
unifyall(Def, A).
expr(lam(V1, V2, Body), C3, fn(A1, A2, B)) :-
expr(Body, C1, B),
split(V1, C1, D1, C2),
split(V2, C2, D2, C3),
unifyall(D1, A1),
unifyall(D2, A2).
expr(let(Var, Body, Rhs), Cxt, T2) :-
expr(Body, C1, T1),
expr(Rhs, C2, T2),
split(Var, C2, Def, C3),
unifyeach(Def, pair(C1, T1), C4),
append(C4, C3, Cxt).
We get correct results:
:- expr(app(lam(x, lam(y, pair(var(x), var(y)))), bool(true), bool(false)),
Cxt, Typ).
yes(Cxt6 = nil, Typ1 = prod(bool, bool)).
:- expr(app(app(lam(x, y, pair(var(x), var(y))), bool(true)), bool(false)),
Cxt, Typ).
NP.
:- expr(
let(h, lam(x, lam(y, pair(var(x), var(y)))),
let(g, lam(f, app(var(f), bool(true), bool(false))),
app(var(g), var(h))
)
),
Cxt, Typ).
yes(Cxt6 = nil, Typ1 = prod(bool, bool)).
:- expr(
let(h, lam(x, y, pair(var(x), var(y))),
let(g, lam(f, app(app(var(f), bool(true)), bool(false))),
app(var(g), var(h))
)
),
Cxt, Typ).
NP.
Keean.
On 25 February 2015 at 08:26, Matt Oliveri <[email protected]> wrote:
> 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
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
