User loginNavigation 
Recursive typesIn some literature, including Wikipedia, there is a distinction I don't quite understand made between isorecursive and eqirecursive typing. In both cases, however, there is a concept of unrolling a recursive type by replacing the fixpoint variable with the recursive term. I believe this idea is suboptimal and should be replaced by a better one I shall describe below. I am interested if this has been done before, and if my analysis (and the concrete algorithm I have written) is correct. The problem with isorecursion is that it induces an equivalence relation on type representations, and this a partition, which fails to place eqiequivalent types in the same class. Here is an example: ([] > [([] > fix2)]) Here [..] denotes an nary tuple type, > is a function type, and fix2 is a fixpoint whose binder is implicitly 2 levels up in the structure. These encodings represent the same type, the second one is recursive but its unrolling is not equal to the first type. I have found a solution to this problem: instead of a full unrolling, we can just unroll one level. This is much better! In particular my rerolling algorithm subsumes the standard rerolling by a full circle, and also produces a unique canonical representative of the class. It should work for monomorphic and first order polymophic types, at least if there is only a single fixpoint. I will not give the algorithm here but I will give a description because it is fun! Consider a piece of string representing your type, with coloured segments for each level. The end of the string is knotted around the string some way up. The knot is called the fixpoint and the place it is knotted to is called the binding point. The algorithm for rerolling the string simply rolls the circle up the string one segment and compares the colours. If they're equal, roll up another segment. Continue until you either run out of string, or you get a mismatch, in which case backtrack by one. You can finish by cutting the matching tail off and doing a new knot. Unrolling is the same. Just unroll ONE segment to shift the fixpoint binder down out of the way. A standalone demo in Ocaml is here: https://github.com/felixlang/felix/blob/master/m.ml By skaller at 20160610 16:17  LtU Forum  previous forum topic  next forum topic  other blogs  7499 reads

Browse archivesActive forum topics 
Recent comments
5 hours 20 min ago
5 hours 38 min ago
5 hours 42 min ago
2 days 2 hours ago
2 days 11 hours ago
2 days 18 hours ago
2 days 19 hours ago
3 days 2 hours ago
3 days 3 hours ago
3 days 5 hours ago