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  5699 reads

Browse archivesActive forum topics 
Recent comments
1 hour 47 min ago
5 hours 56 min ago
8 hours 2 min ago
11 hours 43 min ago
21 hours 57 min ago
22 hours 43 min ago
1 day 1 hour ago
1 day 8 hours ago
1 day 11 hours ago
1 day 13 hours ago