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

Browse archivesActive forum topics 
Recent comments
4 hours 38 min ago
2 days 11 hours ago
2 days 12 hours ago
3 days 5 hours ago
1 week 15 min ago
1 week 6 hours ago
1 week 8 hours ago
1 week 18 hours ago
1 week 2 days ago
1 week 3 days ago