Coinductive semantics
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  skaller <skaller@u...> 
Subject:  Re: [Camllist] Coinductive semantics 
On Sun, 20060122 at 13:23 +0100, Andrej Bauer wrote: > skaller wrote: > If everyone believed in type theory, compilers would be easy to write. LOL! > Every time a programmer wanted to address an element of an array, he > would provide not just the index k but also the proof p that k is a > valid index. Compiler would just have to check that p is a valid proof > (easy when p is a formal proof). But programmers don't want to do that. Actually some of us would like to do it .. however this is moving past my real problem. I'm willing to accept that the typing may end up being unsound in the sense the compiler cannot prove what it needs to: this is actually easy to fix, by simply inserting a runtime check. Also, in this particular case (arrays) the run time representation is already known (literally it is the same as a variant, where the discriminant tag is the array length). This is very nice, since you can actually match on it against particular constant lengths. My problem is more categorical: given your explanation that this is a dependent typing thing, how do I represent such typing in the compiler? If the type of the *value* of the array bound is a unitsum, what is the type of the store containing that value? In particular if I have a match: match somearray_of_float with  (case 1 of NAT) data => ... // 0 elements  (case 2 of NAT) data => ... // 1 elements  (case ?n of NAT) data => // n1 elements what is NAT? At present my type system only has terms like: type t = [  `tuple of t list  `sum of t list  `unitsum of int ... so they're all just constants. How do I modify the type system to allow for a variable? Do I have to actually put executable terms into the type terms? That would account for construction, what about destructors (pattern matches)? Clearly the match has to get out a run time representation of the length .. but it isn't an integer: I mean, the encoding at run time is certainly an integer .. but what is the type ascribed to this value? I called it NAT above .. what, categorically, is NAT? BTW: I think all this analysis could apply to Ocaml too.  John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net