hybridtypesystem 0.2
The Hybrid Type System
Row + Implicit arguments + MLF(WIP).
Notes about System F
Before implementing MLF:
choose: forall a. a -> a -> a
auto : forall a. a -> a
(choose auto) : (forall a. a —> a) -> (forall a. a -> a)
// if auto is defined without annotations, polymorphisms of lambdas get lost
auto2 : a -> a
(choose auto) : (a -> a) -> (a -> a)
Notes about System F-Omega
Kind checker is not implemented.
Usage
from hybridts.tc_state import TCState
from hybridts.type_encoding import row_of_map, record_of_row, poly_row, empty_row
tctx = {}
tcs = TCState(tctx)
x1 = tcs.new_var()
x2 = tcs.new_var()
int_t = tcs.mk_new_type("base.int") # nominal type
tcs.unify(x1, int_t)
tcs.unify(x1, x2)
assert tcs.infer(x1) == int_t
assert tcs.infer(x2) == int_t
x3 = tcs.new_var()
r1 = row_of_map({'a': x1, 'b': x3}, empty_row)
r1 = record_of_row(r1)
tho = tcs.new_var()
r2 = row_of_map({'a': x3}, poly_row(tho))
r2 = record_of_row(r2)
tcs.unify(r1, r2)
print(tcs.infer(r1))
print(tcs.infer(r2))
# (RecordT, (RowConsT, 'b', (NomT, 'base.int'), (RowConsT, 'a', (NomT, 'base.int'), (RowMonoT,))))
# (RecordT, (RowConsT, 'a', (NomT, 'base.int'), (RowPolyT, (RecordT, (RowConsT, 'b', (NomT, 'base.int'), (RowMonoT,)
For personal and professional use. You cannot resell or redistribute these repositories in their original state.
There are no reviews.