Most of the time instantiation is actually O(n log n), this mostly don't matter as types are always small. But for big types by having an additional memory cell on every type, an array / vector can be created.
Doesn't matter how forall is encoded, instantiation needs to copy all sections of a type that may include an occurence of the free variable being instantiated.
Maybe an additional branching can be used to prevent allocation.
type level = int
(*
every arrow contains a forall
level of the arrow = level of forall
advantages:
types contain a single node
generic functions have smaller types
disadvantages:
subsumption is a lot more_ costly
level of arrow cannot be used on optimizations
*)
type typ =
| TVar of level
| TArrow of level * typ * typ
(*
forall variant
every expression that introduces a new variable will automatically insert a forall
generalization can happen by just attaching a TForall on the beginning with the level on every lambda
*)
type typ =
| TVar of level
| TArrow of typ * typ
| TForall of level * typ
(* mutable level
advantages:
changing the level of all types *)
type typ =
| TVar of level
| TArrow of typ * typ
| TForall of level * typ
Because we do generalization on every arrow efficiently, a let that doesn't introduce a type doesn't actually need to introduce a region as there is no possible type to escape, which also means simple lets will never need to iterate over the return type.
A possible thing is to ensure that the level always increases, so that no two types in different blocks will ever have the same level. Can we somehow ensure that no type will ever have the same level at all?
This allows to simple reasoning of the problems as it avoids possible problems like potential free variable generic capture.
The level is a concept introduced by the typer that delimits the region that a variable lives
A type cannot ever escape it's scope, so if a variable was introduced on a level X it cannot be set to a type of level X + 1 as that would mean the type is used before being defined.
So the level of a variable can only be reduced, this with this we can also do generalization, if the level of the variable is the same as when it was introduced, that means the variable is not a free variable in the scope and can be generalized.
We use negative numbers for universally generalized types, essentially forall encoding, so that they always have a smaller type, than the place where they're being used, this is important so that we can pass a type introduced at X to a generic function introduced at X - 1.
Effectively that's the same as using a single bit to decide if a type is generic or not.
When instantiating this type 'a[-2] -[2]> 'b[-3] -[-3]> 'a, do we need to actually copy the 'b[-3]? That would be the case for the typer described by Oleg already but we may have room for updates.
A cool optimization trick would be to know how many levels deep we have an use an array for it, so we know where to find the variables in O(1). This only works if we have always small generic levels tho or we can store both the smallest generic level on the type and also the biggest generic level on the type.
An alternative that works even if levels are really deep, is to we can still rely on a hashtbl and have it to verify how deep.
(* val false inference *)
forall a. a -> forall b. b -> b
'a[-2] -[2]> 'b[-3] -[3]> 'b
(* simple instantiation *)
inst(a -> forall b. b -> b)
'a[1] -[1]> 'b[-2] -[2]> 'b
(* possible instantiation, short circuits on the generic *)
inst(a -> forall b. b -> b)
'a[1] -[1]> 'b[-3] -[3]> 'b
(* val true inference *)
forall a. a -> forall b. b -> a
'a[-2] -[2]> 'b[-3] -[-3]> 'a
(* simple instantiation *)
'a[1] -[1]> 'b[-2] -[2]> 'a
(* possible instantiation, avoids allocation of var 'b *)
'a[1] -[1]> 'b[-3] -[3]> 'a
but how to instantiate this:
forall a b. b -> forall c. a -> c
'b[-1] -[1]> ('a[-1] -[-3]> 'c[-3])
(* simple instantiation,
but I believe this requires an additional map from level -> level *)
'b[4] -[4]> ('a[4] -[5]> 'c[-5])
(* simple solution with no additional maps,
this on the other hand can be derived just by doing:
absolute(level) - absolute(base level)
but that breaks how I do my assumptions and allows subtraction of levels
*)
'b[4] -[4]> ('a[4] -[6]> 'c[-6])
(* possible instantiation, avoids allocation of var 'b *)
'b[4] -[4]> ('a[4] -[3]> 'c[-3])Is any variable not preceeded by a forall, they can appear even in the case of a well formed types, as an example in the type forall a. a -> a all variables are quantified, but if we go a single level deep the type a -> a is present but a is not quantified.
This is even the case during typing as fun x -> x will be first typed as a -> a then generalized to forall a. a -> a.
Unification of free variables actually mutate them, this is the main mechanism where inference is achieved, by introducing a free variable in the context.
A generic variable is a variable where at any point was quantified, all generic variables have negative levels. This allow to analyze a type without keeping track of the context as we know that this variable at some point was generalized, particularly useful during instantiation.
As an example we can look on the type forall a[-1]. a -> a where the type a has a negative level, so when analyzing the sub type a[-1] -> a we can immediatily understand that a is quantified even without looking on the parent.
Note that a generic type may still contain non quantified types. TODO: write an example for this
Is a type where all of it's variables
Unlike the typer shown by Oleg we support forall in any position, that requires that composite types have a meaningful level to understand where the forall is defined, without it ambiguity would arise, example:
a[-2] -> a[-2] can mean either forall a. a -> a or (forall a. a) -> (forall a. a). By making so that the arrow itself also has a level we can solve the problem, so a[-1] -[-1]> a[-1] means forall a. a -> a and a[-2] -[-1]> a[-2] means (forall a. a) -> (forall a. a).
One possibility to non generic levels for composite types is that if the absolute value means the level that the variable was introduced then this type does not include any generic free variable, so forall a. a -> a would be a[-1] -[1]> a[-1]. To achieve that during typing we just need to know what is the biggest generic level found and if it is smaller or equal than the current level, there is no generic free variable inside of it.
This matches the Oleg typer in the sense that non generic levels don't need to be scanned during instantiation. A difference is that a true non generic composite type will still be instantiated, but I believe that because they're reduced as soon as they're used they will not be
But a good thing would be proof the above is sound. I truly have problems to accepting that it is sound
(* forall b. a -> b *)
(* a := forall a. a -> c -> a *)
(* forall b. (forall a. a -> c -> a) -> b *)
'a[1] -[2]> 'b[-2]
'a[1] := 'a[-2] -[-2]> 'c[1] -> 'a[-2]
('a[-2] -[-2]> 'c[1] -> 'a[-2]) -[2]> 'b[-2]
(* forall a b. (a -> c -> a) -> b *)
('a[-1] -[-1]> 'a[-1]) -[-1] -> 'b[-1]
'a[-1] -[+1]> ('b[-2] -[-2]> 'a[-1])Maybe I need to instantiate the type every time I do a set_var? If so I can just have a wrapper and have it being lazy.
But also, when do I need to instantiate the type on a set_var? Maybe instead of instantiation is just a matter of copying it?
Some properties:
the level will always be bigger or equal to the biggest level of it's quantified variables
- Why?
- Proof?
the level will always be smaller or equal to the biggest level of it's free variables
- Why?
- Proof?
A non generic composity type doesn't contain it will never contains a generic free variables
- Why?
My hypothesis is that this type will never be created
- Proof?
forall a.
This is a list of problematic types that makes me want to overengineer it.
This is currently not possible due types where the parent type is present, example:
forall a. a -> forall a. b -> a which has the following encoding a[-1] -[-1]> (b[-2] -[-2]> a[-1])
A possibility to do that would be to make so that composite types also contain an additional level indicator, pointing if the type contains any free variables. I belive that can be done without needing to scan multiple types the types.
I think this is solved already by the non ge
let sequence0 : 'a[2] -[2]> ('b[1] -[1]> 'b[1])
let sequence1 : 'a[5] -[5]> ('b[3] -[3]> 'b[3])
let sequence2 : 'a[6] -[6]> ('b[6] -[6]> 'b[6])
type 'a t = 'a -> 'a constraint 'a >= ('a. 'a -> 'a)
let chose_id : 'a. 'a -> 'a constraint 'a >= ('a. 'a -> 'a) = choose id
'a. 'a -> 'a -> 'a
('a. 'a -> 'a -> 'a) ('a. 'a -> 'a)
'a. ('a. 'a -> 'a -> 'a) ('a -> 'a)
'a. ('a -> 'a) -> ('a -> 'a)
('a. 'a -> 'a) -> ('a. 'a -> 'a)Which type should be the following inferred as?
let apply: 'a. (int -> 'a) -> unit = fun f -> let _ = f 1 in ()
(* or *)
let apply: ('a. int -> 'a) -> unit = fun f -> let _ = f 1 in ()
(* or *)
let apply: (int -> 'a. 'a) -> unit = fun f -> let _ = f 1 in ()
type id = 'a. 'a -> 'a
let choose: 'a. 'a -> 'a -> 'a
let id: 'a. 'a -> 'a
let apply_id: 'b. ('a. id) -> 'b -> 'b
let choose_apply_id: ('b. ('a. 'a id) -> 'b id) -> unit
let choose_apply_id: 'b. (('a. 'a id) -> 'b id) -> unit
let choose_apply_id: 'a. 'b. ('a id) -> 'b id) -> unit
let id: 'a. 'a -> 'a = fun x -> x
let id = (id: ('a. 'a -> 'a) -> 'a. 'a -> 'a) id
type id = 'a. 'a -> 'a
type apply_id = 'a. id -> 'a -> 'a
type apply_apply_id = 'a. apply_id -> 'a -> 'a
type apply_apply_id = 'a. ('a. ('a. 'a -> 'a) -> 'a -> 'a) -> 'a -> 'a
let apply_id: ('a. 'a -> 'a) -> 'a -> 'a
let apply_apply_id:When applying a function we always choose to reduce the variable to the minimum possible ranked type, so that there will never be a case where flexible types are required.
If parameter is rank-0 then argument is instantiated. Otherwise just compare We always instantiate the argument unless the argument and the expected type have the same polymorphic rank.
So if a parameter expects a type of rank-0 and it is provided with a parameter of rank-1 we instantiate it, moving to rank-0.
Types can always be moved to the same by doing current_type.level - base_type.level
(* if the level was int | type, we could do reference counting and prevent a forall with no variables *)
(* simple: just set received to expected if received is more_ general *)
(* accepted *)
val expected: 'a[1] -[1]> ('b[1] -[2]> 'b[1])
val received: 'a[1] -[1]> ('b[2] -[2]> 'b[2])
(* rejected *)
val expected: 'a[1] -[1]> ('b[2] -[2]> 'b[2])
val received: 'a[1] -[1]> ('b[1] -[2]> 'b[1])
(* *)
val expected: 'a[1] -[1]> ('b[2] -[2]> 'b[2])
val received: 'a[1] -[1]> ('b[3] -[3]> 'b[3])
val expected: 'a[1] -[1]> ('b[3] -[3]> 'b[3])
val received: 'a[1] -[1]> ('b[2] -[2]> 'b[2])
val expected: 'f. (('a. 'a -> 'a -> 'a) as 'f) -> 'f
val received: ('a. 'a -> 'b. 'b -> 'b) -> _
val expected: 'f. (('a. 'a -> 'a -> 'a) as 'f) -> 'f
val received: ('a. 'b. 'a -> 'b -> 'b) -> _
val expected: 'f. (('a. 'a -> 'a -> 'a) as 'f) -> 'f
val received: ('a. 'a -> 'b. 'b -> 'b) -> _
val f: 'f. (('a. 'b. 'a -> 'b -> 'b) as 'f) -> 'f
Any let that is used only once doesn't need to be instantiated or generalized, this is quite common, use pass before typing to get levels and counter on how many usages of ident, this can optimize quite a lot of code.
In a system using levels an weakvar has a level before the base of the current types being unified, otherwise it would be a generic type.
Also to generalize everything under it.
a[_2] -[_2]> a[_2]
_2 := 1;
a[1] -[1]> a[1]
What are the advantages of putting a forall only when it's needed?
-- rejected
expected :: forall a b. a -> b -> forall c. c -> ()
received :: forall a b. a -> forall c. b -> c -> ()
-- this shows a problem with the strategy of only adding the needed foralls
-- it would probably be resolved by instantiating on the second arrow so that -[2]> becomes -[1]>
expected :: a[1] -[1]> b[1] -[1]> c[2] -[2]> ()
received :: a[1] -[1]> b[1] -[2]> c[2] -[2]> ()
-- on expected level 2 is not used
expected :: a[1] -[1]> b[1] -[2]> c[3] -[3]> ()
received :: a[1] -[1]> b[1] -[2]> c[2] -[3]> ()
-- accepted
expected :: forall a b. a -> b -> b
received :: forall a. a -> forall b. b -> b
-- this requires to iterate over the return
-- or having the level reference be unique
expected :: a[1] -[1]> b[1] -[1]> b[1]
received :: a[1] -[1]> b[2] -[2]> b[2]
-- no iteration or shared level reference required
expected :: a[1] -[1]> b[1] -[2]> b[1]
received :: a[1] -[1]> b[2] -[2]> b[2]
-- accepted
expected :: forall a. (forall b. b -> b) -> a -> a
received :: forall a. (forall b. b -> b) -> a -> a
-- Co
expected :: (b[2] -[2]> b[2]) -[1]> a[1] -[2]> a[1]
received :: (b[4] -[4]> b[4]) -[3]> a[3] -[4]> a[3]
-- param, Contra
received :: (b[2] -[2]> b[2])
expected :: (b[4] -[4]> b[4])
This typer uses a reference to a level instead of the level itself inside of subtype so that we can tag all variables as expected easily.
Variance and maybe if it's even or odd
expected :: (forall ai. ai[2]) -> forall ai. ai[2]
received :: (forall aj. aj[2]) -> forall aj. aj[2]
received :: forall ai. ai[2]
expected :: forall aj. aj[2]id :: forall a. a -> a
id x = x
call_id :: (forall a. a -> a) -> forall b. b -> b
call_id :: (a[1] -[1]> a[1]) -[0]> b[1] -[1]> b[1]
call_id id x = id x
sequence :: forall a. a -> forall b. b -> b
sequence a b = b
id_sequence :: _a -> _b -> _b
id_sequence = id sequenceuniversal: A. A;
f: _a -> B. B -> B = universal
expr = (A[0]. (id: A -> A) -> () -> id) (A[1]. (x: A) -> x)
Id: A. A -> A;
f: Id[1] -[0]> Id[1] -[0]> Id[1]
x = (((id1: Id[1]) -[0]> (id2: Id[2]) -[1]> id2)
(A[0]. (x: A) -> x))
(A[0]. (x: A) -> x);
(x -> x): (A. A -> A)-- accepted
expected :: forall a. forall b. a -> b -> b
received :: forall a. a -> forall b. b -> b
-- rejected
expected :: forall a. a -> forall b. b -> b
received :: forall c. forall d. c -> d -> d
t :: forall a. a -> forall b. b -> b
t :: a[0] -[0]> b[1] -[1]> b[1]
t :: forall a. forall b. a -> b -> b
t :: a[0] -[0]> b[0] -[1]> b[0]
t :: (forall a. a -> a) -> () -> forall b. b -> b
t :: (a[1] -[1]> a[1]) -[0]> () -[1]> _b[2] -[_2]> _b[2]
t :: forall b. (forall a. a -> a) -> () -> b -> b
t :: (a[1] -[3:1]> a[1]) -[0:0]> () -[1:0]> b[0:0] -[2:0]> b[0:0]
t :: (forall a. a -> a) -> () -> forall b. b -> b
t :: (a[1] -[1]> a[1]) -[0:0]> () -[1:0]> b[2:0] -[2:0]> b[2:0]
t :: a[1] -[1]> a[1]
t :: forall a. (a -> a) -> ()
t :: (a[0] -[1]> a[0]) -[0]> ()
expected :: (forall a. a -> a) -> (forall b. b -> b) -> forall c. c -> c
expected :: (a[1] -[1]> a) -[0]> (b[2] -[2]> b) -[1]> c[2] -[2]> c
-- rejected
expected :: forall a. a -> forall b. b -> b
received :: forall c. forall d. c -> d -> d
expected :: a[0] -[0]> b[1] -[1]> b[1]
received :: c[0] -[0]> d[0] -[1]> d[0]
expected :: a[0] -[0]> b[0] -[1]> b[0]
received :: _c[0] -[0]> _d[0] -[1]> _d[0] -- weaken 0
received :: a[0]
expected :: _c[0] -- c := a[0]
expected :: b[1] -[1]> b[1]
received :: _d[0] -[1]> _d[0] -- weaken 1
received :: b[1]
expected :: _d[0] -- FAILS
-- rejected
expected :: a[0:0] -[0:0]> b[1:0] -[1:0]> b[1:0]
received :: c[2:0] -[2:0]> d[2:0] -[3:0]> d[2:0]
expected :: a[0:0] -[0:0]> b[1:0] -[1:0]> b[1:0]
received :: _c[2:0] -[2:0]> _d[2:0] -[3:0]> _d[2:0] -- weaken 2
expected :: a[0:0] -[0:0]> b[1:0] -[1:0]> b[1:0]
received :: c[0:0] -[0:0]> d[0:0] -[3:0]> d[0:0] -- unify arrow
received :: a[0:0]
expected :: c[0:0] -- c := a[0:0]
expected :: b[1:0] -[1:0]> b[1:0]
received :: d[0:0] -[3:0]> d[0:0] -- weaken 3
expected :: b[1:0] -[1:0]> b[1:0]
received :: d[0:0] -[1:0]> d[0:0] -- unify arrow
received :: b[1:0]
expected :: d[0:0]
-- accepted
expected :: a[0:0] -[0:0]> b[0:0] -[1:0]> b[0:0]
received :: c[2:0] -[2:0]> d[3:0] -[3:0]> d[3:0]
expected :: a[0:0] -[0:0]> b[0:0] -[1:0]> b[0:0]
received :: _c[2:0] -[2:0]> d[3:0] -[3:0]> d[3:0] -- weaken 2
expected :: a[0:0] -[0:0]> b[0:0] -[1:0]> b[0:0]
received :: c[0:0] -[0:0]> d[3:0] -[3:0]> d[3:0] -- unify arrow
received :: a[0:0]
expected :: c[0:0] -- c := a[0:0]
expected :: b[0:0] -[1:0]> b[0:0]
received :: _d[3:0] -[3:0]> _d[3:0] -- weaken 3
expected :: b[0:0] -[1:0]> b[0:0]
received :: d[1:0] -[1:0]> d[1:0] -- unify arrow
expected :: forall a. a -> a
received :: forall b. b
expected :: a[0] -[0]> a[0]
received :: b[0]
expected :: forall a. forall b. a -> b -> b
received :: forall c. c -> c -> c
-- rejected
expected :: a[0] -[0]> b[0] -[1]> b
received :: c[0] -[0]> c -[1]> c
received :: a[0]
expected :: _c[0] -- c := a[0]
expected :: b[0] -[1]> b
received :: a[0] -[1]> a
received :: b[0]
expected :: a[0]
id :: a[0] -[0]> a[0]
id' :: a[1] -[1]> a[1]
-- rejected
expected :: a[x:0] -[x:0]> b[y:0] -[y:0]> b[y:0]
received :: c[z:0] -[z:0]> d[z:0] -[r:0]> d[z:0]
-- accepted
expected :: a[x:0] -[x:0]> b[x:0] -[y:0]> b[x:0]
received :: c[z:0] -[z:0]> d[r:0] -[r:0]> d[r:0]
-- rejected
expected :: a[x] -[x]> b[y] -[y]> b[y]
received :: c[z] -[z]> d[z] -[r]> d[z]
-- accepted
expected :: a[x] -[x]> b[x] -[y]> b[x]
received :: c[z] -[z]> d[r] -[r]> d[r]
expected :: a[x:0] -[x:0]> b[x:0] -[y]> b[x:0]
received :: _c[z:0] -[z:0]> d[r] -[r]> d[r] -- weaken z; z := 0; x := 0
received :: a[x:0]
expected :: _c[z:0] -- c := a[x:0]
expected :: b[x:0] -[y:1]> b[x:0]
received :: _d[r:1] -[r:1]> _d[r:1] -- weaken r; r := 1; y := 1
received :: b[x:0]
expected :: _d[r:1] -- d := b[x:0]
expected :: b[x:0]
received :: b[x:0]
expected :: a[x] -[x]> b[x] -[y]> b[x]
received :: c[z:0] -[z:0]> d[r] -[r]> d[r] -- weaken z; z := 0
expected :: a[0:0] -[0:0]> b[1:0] -[1:0]> b[1:0]
received :: _c[2:0] -[2:0]> _d[2:0] -[3:0]> _d[2:0] -- weaken 2
expected :: forall a. forall b. a -> b -> b
received :: forall a. a -> a -> a
expected :: a[x] -> b[x] -> b[x]
received :: b[y] -> b[y] -> b[y]
expected :: a[x] -> b[x] -> b[x]
received :: _b[y] -> _b[y] -> _b[y]
expected :: (forall a. a) -> (forall b. b)
received :: forall c. c -> c
expected :: a[4] -[0]> b[4]
received :: c[0] -[0]> c[0]
received :: a[4]
expected :: c[0] -- c := _a[5]
expected :: b[4]
received :: _a[5]
final :: b[4] -[0]> b[4]
expected :: forall a. forall b. a -> b
received :: forall c. c -> c
-- subtype
expected :: a[0] -[0]> b[0]
received :: c[0] -[0]> c[0]
-- subtype_forall
expected :: a[0] -[0]> b[0]
received :: _c[0] -[0]> _c[0]
received :: a[0]
expected :: _c[0] -- c := a[0]
expected :: b[0]
received :: a[0]
expected :: () -> forall a. a -> a
received :: forall a. () -> a -> a
expected :: () -[0]> a[1] -[1]> a[1]
received :: () -[0]> b[0] -[1]> b[0]
expected :: a[1] -[1]> a[1]
received :: _b[0] -[1]> _b[0]
received :: a[1]
expected :: _b[0] -- b := a[1]
expected :: a[1]
received :: _b[0]Write about this somewhere in a proper formal way, also validate the chosen ideas against someone smarter.