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

Browse archivesActive forum topics 
Recent comments
1 hour 29 min ago
5 hours 8 min ago
11 hours 44 min ago
13 hours 12 min ago
17 hours 22 min ago
17 hours 39 min ago
19 hours 26 min ago
20 hours 11 min ago
23 hours 3 min ago
23 hours 20 min ago