User loginNavigation 
Rank0 Intersection Type SystemIn the thread on value level programming we started discussing an HM (like) type system with principal typings. Although based on Olaf Chitil and Grego Erdi's work, it seems what I have implemented has significant differences. There is also some influence from Kfoury and Well's SystemI and SystemE. Key differences: There is no type environment (as it is compositional), and the typing context is a multiset instead of a set. This seems equivalent to allowing rank1 intersection types in the context, but by keeping the types themselves free of intersection operators, a normal HM unification operation can be used, which is decidable. A few key claims: It is decidable, compositional, and has principal typings.  I would like comments on the notation for the formal description of the type system, can it be improved?  I tend to assume everything has been done before, but looking back this seems more original than I thought? Has anyone seen this before or can I count this as its first publication? As the multiset context effectively allows rank1 intersections in the context, but not in the types themselves, a rank0 intersection type seems a good term for this. So here's my first attempt at writing the rules: Rank 0 Intersection Type System Definition:  LIT {}  N : Int  VAR {x : a}  x : a where new a M1  E1 : t1 M2  E2 : t2  APP M  E1 E2 : t where new a SUBS = t1 unify (t2 > a) M = SUBS(M1 multisetunion M2) t = SUBS(a) M1  E1 : t1  ABS M  \x . E1 : t where new a SUBS = emptysubstitutionlist for t' in M1(x): SUBS = SUBS append (SUBS(a) unify SUBS(t')) M = SUBS(M1  x) t = SUBS(a > t1) M1  E1 : t1 M2  E2 : t2  LET M  let x = E1 in E2 : t where SUBS = emtpysubstitutionlist M' = M2  x for t' in M2(x): (M1' t1') = SUBS(M1 t1) with fresh free variables SUBS = SUBS append (SUBS(t') unify t1') M' = M' multisetunion M1' M = SUBS(M') t = SUBS(t2) By Keean Schupke at 20140508 07:50  LtU Forum  previous forum topic  next forum topic  other blogs  5210 reads

Browse archives
Active forum topics 
Recent comments
3 hours 21 min ago
6 hours 12 min ago
7 hours 11 min ago
7 hours 26 min ago
7 hours 51 min ago
8 hours 33 min ago
14 hours 14 min ago
17 hours 30 min ago
1 day 1 hour ago
1 day 3 hours ago