Jonathan S. Shapiro wrote:
> Related to all this, has anybody seen work on what might be termed
> "conditionally dependent types"? That is, a system where I can write
> something like
>
> div: x:int y:int -> { x == 0 => Raise DivideByZero; x != 0 => int }
>
> ? Is this just match types?
There are essentially two ways to support types like this in a
dependent type system. One is to support pattern matching function
types primitively; the other is to support them via intersection types.
I think essentially all dependent type systems that aim to be reasonably
expressive do support this in one way or another.
The approach using intersection types is a little more expressive,
and the pattern matching approach is basically a special case of it
(at least, that's the way I find it most useful to think about it).
If we separate out the issue of exceptions by having div return a
'Maybe int' (defined in the obvious way), then we have:
div: (x:{0} y:int -> Nothing) /\ (x:(int != 0) y:int -> Some int)
The interpretation of a function type used here is that 'S -> T' is
the type of functions that will return something of type T for inputs
of type S, but might return anything for inputs not of type S. So we
can use intersections of function types to specify what the function
returns for various input types.
If the type system also supports declaring exceptions for function
types, then the original example can be written directly as:
div: (x:{0} y:int -> ⊥ raise DivideByZero) /\ (x:(int != 0) y:int -> int)
The concrete syntax could support writing that in the way you wrote it
above, of course.
['⊥' is bottom, if your mail reader doesn't display it correctly.]
--
David-Sarah Hopwood ⚥
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
