Re: [Caml-list] Coinductive semantics

[skaller <skaller@users.sourceforge.net>]

On Sun, 2006-01-22 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 =>    // n-1 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