dependent typed in Qi II

[Mark Tarver]

Somebody wrote to me ....

QUOTE
I am trying to have a function 'g' that takes two numbers with the
value of that number encoded in the type that returns a number that is
the sum of these two numbers such that the type-system knows it is an
addition.

Can you show how it should be done?
UNQUOTE

The correct definition is:

(datatype num

if (number? N)
____________
N : (num N);

M : (num M); N : (num N);
_________________________
(+ M N) : (num (M + N));)

(define add
{(num M) --> (num N) --> (num (M + N))}
M N -> (+ M N))

Qi I does not handle dependent types easily and does not verify this
function because it does not recognise that the variables in the
signature have anything to do with the variables in the body of the
function. I was meaning to fix that and in Qi II I've done so.

Qi II does recognise this dependency and consequently the function
type checks.

(9+) (add 5 6)
11 : (num (5 + 6))

Mark

[Raoul Duke]

> [dependent types] I was meaning to fix that and in Qi II I've done so.

woah, that sounds pretty keen! seems to me from what little i know
that dependent types at compile time are very interesting and have
been sort of only a research topic unless you use Haskell and are
named Oleg, or like fiddling with academic systems like Epigram etc.,
so it is pretty nifty if Qi II can bring it to the masses. remind me
to learn about that when i have a spare moment and lots of coffee...
:-)