diff --git a/deques.ml b/deques.ml index a9c2cb2..5eca303 100644 --- a/deques.ml +++ b/deques.ml @@ -194,204 +194,6 @@ module DequesColorsStack = struct end open DequesColorsStack -module TypeLevelFunctions1 = struct - (* TODO: bundle together the stack and an on-demand infinite stack of free variables *) - (* This should not be exported in the sig. *) - module Private = struct - (* stack of type-level operands *) - type start = () - type ('head, 'tail) stk = Stk of 'head * 'tail (* constraint 'tail = ('a,'b) stk *) - - (* internal: quote a type and place it on the stack *) - type 't _typ = Typ of 't - end - open Private - - (* unwrap the single element on the stack *) - type 'stk return = 'returned constraint 'stk = (start, 'returned _typ) stk - - (* quote a type and place it on the stack *) - type ('stk, 't) typ = ('stk, 't _typ) stk - - (* type-level booleans *) - type ('stk, 'freevar) tru = ('stk, ('a * 'b * 'b)) stk constraint 'freevar = 'a * 'b - type ('stk, 'freevar) fals = ('stk, ('a * 'b * 'b)) stk constraint 'freevar = 'a * 'b - - (* type-level conditional *) - type 'stk ifelse = ('tail, 'tresult) stk - constraint 'tcondition = 'tthen * 'telse * 'tresult - constraint 'stk = ((('tail, 'tcondition) stk, 'tthen) stk, 'telse) stk - - (* type-level duplication of a boolean - - We prefer not to allow duplication of a quoted type, as there would be no - way to avoid using the same polymorphic variables in both occurrences. *) - (* TODO: use if to duplicate! *) - type 'stk dup = ('stk, 'head) stk constraint 'stk = ('tail, 'head) stk - - (* type 'x push = 'a * 'b constraint 'x = 'a * 'b *) - (* type ('tcondition, 'tthen, 'telse) ifelse = 'tresult constraint 'tcondition = 'tthen * 'telse * 'tresult *) - - type s = ((((start, 't) tru, string) typ), int) typ ifelse return -end - - - - - - - - -(* Unification in the HM type system, along with OCaml's constraint keyword, - allows us to describe relations between types. The type-level functions - below are using this in a way that is reminiscent of Prolog's - predicates. We try to put the results on the left-hand side of the equals - sign, even though a use of the constraint keyword establishes an unordered - relation between two types. This explains why it is possible to write - constraint 'x = ('hd, 'tl) push to indicate that 'x is the result, and the - equivalent constraint ('hd, 'tl) push = 'x to indicate that 'hd and 'tl are - expected to be extracted from a known 'x. *) -module T = struct - (* TODO: bundle together the stack and an on-demand infinite stack of free variables *) - (* This should not be exported in the sig. *) - module Private = struct - (* stack of type-level operands *) - type ('tl, 'hd, 'fv) _stack = Stack of 'tl * 'hd * 'fv - type ('stack, 'freevars) _state = State of 'stack * 'freevars (* constraint 'tail = ('a,'b) state *) - - type __start = () - type 'freevars _start = (__start, 'freevars) _state - (* internal: quote a type and place it on the stack *) - type 't _typ = Typ of 't - type 't _polytyp = PolyTyp of 't - - (* Push a new type-level value onto the stack *) - (* 'fv denotes the free variables in 'v, which will be bound to a dummy - type if the value 'v is dropped from the stack. *) - type ('state, 'v, 'fv) _push = (('stack, 'v, 'fv) _stack, 'freevars) _state - constraint ('stack, 'freevars) _state = 'state - - (* fetch the value on top of the the stack and its free variables *) - type 'state _peekv = 'v - constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state - type 'state _peekfv = 'fv - constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state - - (* drop the value on top of the the stack *) - (* type closed_freevar = [`FreeVar of (closed_freevar * closed_freevar)] *) - type closed_freevar1 = [`FreeVar of unit * unit] - (* 'x serves as a handled. If is is not unified with anything, it does not - cause any harm. If it is unified with ('u * 'u * 'v * 'v * 'w * 'w), it - causes three pairs of types to unify, thereby closing a local type - variable and propagating that close order down to the two children. *) - type 'dummy close_freevars = ('u * 'u * 'v * 'v * 'w * 'w) constraint ('u * 'v * 'w) = 'dummy - type ('a, 'x) _fv = [`FreeVar of 'a * 'x] - constraint ( 'a * closed_freevar1 - * unit * unit (* ignored *) - * unit * unit (* ignored *)) = 'x - type ('a, 'b, 'x) _fvs = [`FreeVar of ('a * 'b) * 'x] - constraint ( unit * unit (* ignored *) - * 'a * [`FreeVar of 'one * 'dummy1 close_freevars] - * 'b * [`FreeVar of 'two * 'dummy2 close_freevars]) = 'x - (*TODO: possibly need to bind: 'one 'two 'dummy1 'dummy2 *) - type no_freevar = closed_freevar1 - type 'state _pop = ('tail, 'freevars) _state - constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state - type 'state _discard = ('tail, 'freevars) _state - constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state - constraint 'fv = [`FreeVar of 'fv_ * 'dummy close_freevars] - end - open Private - - (* Instantiate a new free variable. *) - type ('state, 'freevar) _freevar = ('stack, 'new_freevars) _state - constraint ('stack, 'freevars) _state = 'state - constraint 'new_freevars * 'freevar = 'freevars - - (* Unwrap the single element on the stack. *) - type 'state return = 'returned - constraint 'state = ((__start, 'returned _typ, 'fvs) _stack, closed_freevar1) _state - constraint 'fvs = [`FreeVar of 'fvs_ * 'dummy close_freevars] - - (* Quote a type and place it on the stack. *) - type ('state, 't) typ = (('stack, 't _typ, no_freevar) _stack, 'freevars) _state - constraint ('stack, 'freevars) _state = 'state - - (* Quote a polymorphic type and place it on the stack. *) - (* 'x should be a free variable on the caller's site, - 'xt should be 'x t where t is the polymorphic type to quote. *) - type ('state, 'x, 'xt) polytyp = (('stack, ('xt * 'x) _polytyp, ('x, 'fv) _fv) _stack, 'freevars) _state - constraint ('stack, 'freevars) _state = ('state, 'x * 'fv) _freevar - - (* type-level booleans *) - type 'state tru = ('state2, ('a * 'b * 'a * 'b), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push - constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar - type 'state fals = ('state2, ('a * 'b * 'b * 'a), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push - constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar - - type ('x, 'y) _cons = Cons of 'x * 'y - type 'state cons = ('state2 _pop _pop, - ('state2 _pop _peekv, 'state2 _peekv) _cons, - ('state2 _pop _peekfv, 'state2 _peekfv, 'fv) _fvs) _push - constraint 'state2 = ('state, 'fv) _freevar - type 'state uncons = (('state _pop, 'x, 'fvx) _push, 'y, 'fvy) _push - constraint ('x, 'y) _cons = 'state _peekv - constraint ('fvx, 'fvy, 'fvxy) _fvs = 'state _peekfv - constraint 'fvxy = ( unit * unit (* ignored *) - * 'a * [`FreeVar of 'one * 'dummy1 close_freevars] - * 'b * [`FreeVar of 'two * 'dummy2 close_freevars]) - - (* type-level conditional *) - type 'state ifelse = (('tail, 'tresult, 'fvr) _stack, 'freevars) _state - constraint 'state = (((('tail, 'tcondition, 'fvc) _stack, 'tthen, 'fvt) _stack, 'telse, 'fve) _stack, 'freevars) _state - constraint 'tcondition = ([`v_fv of 'tthen * 'fvt]) - * ([`v_fv of 'telse * 'fve]) - * ([`v_fv of 'tresult * 'fvr]) - * ([`v_fv of 'tdiscard * 'fvd]) - (* Since the discarded value may contain some free variables, we need to - bind them to some dummy value. *) - constraint 'fvd = [`FreeVar of 'fvd_ * 'dummy close_freevars] - constraint 'fvc = [`FreeVar of 'fvab * 'x] - constraint 'x = unit (* release the 'x of 'fvc, since the condition was used *) - - (* type-level duplication of a boolean - - We prefer not to allow duplication of a quoted type, as there would be no - way to avoid using the same polymorphic variables in both occurrences. *) - type 'state dup = 'state tru tru cons fals fals cons ifelse uncons - type 'state exch = (('state _pop _pop, 'state _peekv, 'state _peekfv) _push, 'state _pop _peekv, 'state _pop _peekfv) _push - type 'state pop = 'state _discard - - (* apply a single-argument polymorphic type to an argument *) - type 'state polyapp = 'result - (* left-hand-side of product type is output, right-hand-side is input *) - constraint ('result * ('state _pop)) _polytyp = 'state _peekv - - (* type 'x push = 'a * 'b constraint 'x = 'a * 'b *) - (* type ('tcondition, 'tthen, 'telse) ifelse = 'tresult constraint 'tcondition = 'tthen * 'telse * 'tresult *) - - type 'state typ_string = ('state, string) typ - type 'state typ_int = ('state, int) typ - type 'state typ_unit = ('state, unit) typ -end - -module TypeLevelFunctionsExamples = struct - open T - - type 'state s = 'state typ_string typ_int ifelse return - type s1 = 't tru s (* push true on the stack, call s => string *) - type s2 = 't fals s (* push false on the stack, call s => int *) - - type 'state f = 'state tru typ_string - type 'state t = 'state polyapp typ_int ifelse return - type 'state push_f = ('state, 'x, 'x f) polytyp - type t1 = 't push_f t (* => string *) - - type 'state u = 'state dup typ_int typ_string ifelse typ_unit exch ifelse return - type u1 = 't tru u - type u2 = 't fals u -end - (** jacm-final.pdf p.8 (584) ยง4.1 media 60 480 368 36 *) (* let rec child i d = if i = 0 then d diff --git a/deques_typelevelprogramming.ml b/deques_typelevelprogramming.ml new file mode 100644 index 0000000..6bbfcc7 --- /dev/null +++ b/deques_typelevelprogramming.ml @@ -0,0 +1,149 @@ +(* Unification in the HM type system, along with OCaml's constraint keyword, + allows us to describe relations between types. The type-level functions + below are using this in a way that is reminiscent of Prolog's + predicates. We try to put the results on the left-hand side of the equals + sign, even though a use of the constraint keyword establishes an unordered + relation between two types. This explains why it is possible to write + constraint 'x = ('hd, 'tl) push to indicate that 'x is the result, and the + equivalent constraint ('hd, 'tl) push = 'x to indicate that 'hd and 'tl are + expected to be extracted from a known 'x. *) +module T = struct + (* TODO: bundle together the stack and an on-demand infinite stack of free variables *) + (* This should not be exported in the sig. *) + module Private = struct + (* stack of type-level operands *) + type ('tl, 'hd, 'fv) _stack = Stack of 'tl * 'hd * 'fv + type ('stack, 'freevars) _state = State of 'stack * 'freevars (* constraint 'tail = ('a,'b) state *) + + type __start = () + type 'freevars _start = (__start, 'freevars) _state + (* internal: quote a type and place it on the stack *) + type 't _typ = Typ of 't + type 't _polytyp = PolyTyp of 't + + (* Push a new type-level value onto the stack *) + (* 'fv denotes the free variables in 'v, which will be bound to a dummy + type if the value 'v is dropped from the stack. *) + type ('state, 'v, 'fv) _push = (('stack, 'v, 'fv) _stack, 'freevars) _state + constraint ('stack, 'freevars) _state = 'state + + (* fetch the value on top of the the stack and its free variables *) + type 'state _peekv = 'v + constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state + type 'state _peekfv = 'fv + constraint (('stack, 'v, 'fv) _stack, 'freevars) _state = 'state + + (* drop the value on top of the the stack *) + (* type closed_freevar = [`FreeVar of (closed_freevar * closed_freevar)] *) + type closed_freevar1 = [`FreeVar of unit * unit] + (* 'x serves as a handled. If is is not unified with anything, it does not + cause any harm. If it is unified with ('u * 'u * 'v * 'v * 'w * 'w), it + causes three pairs of types to unify, thereby closing a local type + variable and propagating that close order down to the two children. *) + type 'dummy close_freevars = ('u * 'u * 'v * 'v * 'w * 'w) constraint ('u * 'v * 'w) = 'dummy + type ('a, 'x) _fv = [`FreeVar of 'a * 'x] + constraint ( 'a * closed_freevar1 + * unit * unit (* ignored *) + * unit * unit (* ignored *)) = 'x + type ('a, 'b, 'x) _fvs = [`FreeVar of ('a * 'b) * 'x] + constraint ( unit * unit (* ignored *) + * 'a * [`FreeVar of 'one * 'dummy1 close_freevars] + * 'b * [`FreeVar of 'two * 'dummy2 close_freevars]) = 'x + (*TODO: possibly need to bind: 'one 'two 'dummy1 'dummy2 *) + type no_freevar = closed_freevar1 + type 'state _pop = ('tail, 'freevars) _state + constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state + type 'state _discard = ('tail, 'freevars) _state + constraint (('tail, 'v, 'fv) _stack, 'freevars) _state = 'state + constraint 'fv = [`FreeVar of 'fv_ * 'dummy close_freevars] + end + open Private + + (* Instantiate a new free variable. *) + type ('state, 'freevar) _freevar = ('stack, 'new_freevars) _state + constraint ('stack, 'freevars) _state = 'state + constraint 'new_freevars * 'freevar = 'freevars + + (* Unwrap the single element on the stack. *) + type 'state return = 'returned + constraint 'state = ((__start, 'returned _typ, 'fvs) _stack, closed_freevar1) _state + constraint 'fvs = [`FreeVar of 'fvs_ * 'dummy close_freevars] + + (* Quote a type and place it on the stack. *) + type ('state, 't) typ = (('stack, 't _typ, no_freevar) _stack, 'freevars) _state + constraint ('stack, 'freevars) _state = 'state + + (* Quote a polymorphic type and place it on the stack. *) + (* 'x should be a free variable on the caller's site, + 'xt should be 'x t where t is the polymorphic type to quote. *) + type ('state, 'x, 'xt) polytyp = (('stack, ('xt * 'x) _polytyp, ('x, 'fv) _fv) _stack, 'freevars) _state + constraint ('stack, 'freevars) _state = ('state, 'x * 'fv) _freevar + + (* type-level booleans *) + type 'state tru = ('state2, ('a * 'b * 'a * 'b), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push + constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar + type 'state fals = ('state2, ('a * 'b * 'b * 'a), (('a, 'fva) _fv, ('b, 'fvb) _fv, 'fvab) _fvs) _push + constraint 'state2 = ('state, 'a * 'b * 'fva * 'fvb * 'fvab) _freevar + + type ('x, 'y) _cons = Cons of 'x * 'y + type 'state cons = ('state2 _pop _pop, + ('state2 _pop _peekv, 'state2 _peekv) _cons, + ('state2 _pop _peekfv, 'state2 _peekfv, 'fv) _fvs) _push + constraint 'state2 = ('state, 'fv) _freevar + type 'state uncons = (('state _pop, 'x, 'fvx) _push, 'y, 'fvy) _push + constraint ('x, 'y) _cons = 'state _peekv + constraint ('fvx, 'fvy, 'fvxy) _fvs = 'state _peekfv + constraint 'fvxy = ( unit * unit (* ignored *) + * 'a * [`FreeVar of 'one * 'dummy1 close_freevars] + * 'b * [`FreeVar of 'two * 'dummy2 close_freevars]) + + (* type-level conditional *) + type 'state ifelse = (('tail, 'tresult, 'fvr) _stack, 'freevars) _state + constraint 'state = (((('tail, 'tcondition, 'fvc) _stack, 'tthen, 'fvt) _stack, 'telse, 'fve) _stack, 'freevars) _state + constraint 'tcondition = ([`v_fv of 'tthen * 'fvt]) + * ([`v_fv of 'telse * 'fve]) + * ([`v_fv of 'tresult * 'fvr]) + * ([`v_fv of 'tdiscard * 'fvd]) + (* Since the discarded value may contain some free variables, we need to + bind them to some dummy value. *) + constraint 'fvd = [`FreeVar of 'fvd_ * 'dummy close_freevars] + constraint 'fvc = [`FreeVar of 'fvab * 'x] + constraint 'x = unit (* release the 'x of 'fvc, since the condition was used *) + + (* type-level duplication of a boolean + + We prefer not to allow duplication of a quoted type, as there would be no + way to avoid using the same polymorphic variables in both occurrences. *) + type 'state dup = 'state tru tru cons fals fals cons ifelse uncons + type 'state exch = (('state _pop _pop, 'state _peekv, 'state _peekfv) _push, 'state _pop _peekv, 'state _pop _peekfv) _push + type 'state pop = 'state _discard + + (* apply a single-argument polymorphic type to an argument *) + type 'state polyapp = 'result + (* left-hand-side of product type is output, right-hand-side is input *) + constraint ('result * ('state _pop)) _polytyp = 'state _peekv + + (* type 'x push = 'a * 'b constraint 'x = 'a * 'b *) + (* type ('tcondition, 'tthen, 'telse) ifelse = 'tresult constraint 'tcondition = 'tthen * 'telse * 'tresult *) + + type 'state typ_string = ('state, string) typ + type 'state typ_int = ('state, int) typ + type 'state typ_unit = ('state, unit) typ +end + +module TypeLevelFunctionsExamples = struct + open T + + type 'state s = 'state typ_string typ_int ifelse return + type s1 = 't tru s (* push true on the stack, call s => string *) + type s2 = 't fals s (* push false on the stack, call s => int *) + + type 'state f = 'state tru typ_string + type 'state t = 'state polyapp typ_int ifelse return + type 'state push_f = ('state, 'x, 'x f) polytyp + type t1 = 't push_f t (* => string *) + + type 'state u = 'state dup typ_int typ_string ifelse typ_unit exch ifelse return + type u1 = 't tru u + type u2 = 't fals u +end