On 24 February 2015 at 17:05, 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.) Actually this is attempting to use shap's notation... so to implement that cast I would do it like this: cast2 f = \x y . (f x) y I'm in the middle of implementing the type inference in a little logic language I wrote, which is like Prolog, but has sound-unification, iterative-deepening search, and constraint-propagation based negation. I have currently got the same inference system as the C++ composition-type-inferencing working, but its much shorter and more readable. I've just implemented concrete arities for (fn 1) and (fn 2) so far. I've attached the code so far at the end. Keean. 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). unifyall(cons(T, Tail), T) :- unifyall(Tail, T). unifyall(nil, T). unifyeach(cons(Tapp, Tail), Tdef) :- duplicate_term(Tdef, Tapp), unifyeach(Tail, Tdef). unifyeach(nil, T). 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(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, T1), append(C1, C3, Cxt). :- expr( let(test1, lam(x, lam(y, pair(var(x), var(y)))), let(cast2, lam(f, lam(x, y, app(app(var(f), var(x)), var(y)))), app(var(cast2), var(test1))) ), Cxt, Typ).
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
