User loginNavigation 
Notation for debugging type derivations.I want to produce traces of the type derivations for compositional type inference to help debugging programs. Currently the reports look like this: var  x : {x : a}  a var  y : {y : a}  a x : {x : a}  a y : {y : a}  a app  (x y) : {x : (a > b), y : a}  b var  z : {z : a}  a (x y) : {x : (a > b), y : a}  b z : {z : a}  a app  ((x y) z) : {x : (a > (b > c)), y : a, z : b}  c However repeating the typings in each derivation seems a bit of a waste of space. I am thinking I can just reference which rule is used and number the statements, a bit like a theorem proof. Something like: 1) var = x : {x : a}  a 2) var = y : {y : a}  a 3) app (1) (2) = (x y) : {x : (a > b), y : a}  b 4) var = z : {z : a}  a 5) app (3) (4) = ((x y) z) : {x : (a > (b > c)), y : a, z : b}  c Does this seem a reasonable notation? it the use of the doubleturnstile "=" a misuse of notation? Is there a better way to write this? By Keean Schupke at 20140605 16:30  LtU Forum  previous forum topic  next forum topic  other blogs  2937 reads

Browse archives
Active forum topics 
Recent comments
2 days 6 hours ago
2 days 17 hours ago
5 days 14 hours ago
6 days 10 hours ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
3 weeks 2 days ago