DML , ML with restricted dependent types

Refering to this paper Dependent ML: An Approach to Practical Programming with Dependent Types

Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a nat directly.

datatype ’a list (int) =
nil(0) | {n:nat} cons(n+1) of ’a * ’a list(n)
fun(’a)
append (nil, ys) = ys
| append (cons (x, xs), ys) = cons (x, append (xs, ys))
withtype {m:nat,n:nat} ’a list(m) * ’a list(n) -> ’a list(m+n)


In there base paper Dependent Types in Practical Programming they have defines it like ’a list of nat which makes more sense :

datatype ’a list = nil | cons of ’a * ’a list
typeref ’a list of nat with (* indexing the datatype ’a list with nat *)
nil <| ’a list(0)
| cons <| {n:nat} ’a * ’a list(n) -> ’a list(n+1)

fun(’a)
append(nil, ys) = ys
| append(cons(x, xs), ys) = cons(x, append(xs, ys))
where append <| {m:nat}{n:nat} ’a list(m) * ’a list(n) -> ’a list(m+n)


The first declaration looks elegant and In second its not clear why to use <| inside where clause ? Can anyone help me with this.

• This is a tough one, but sense you're asking about the specifics of the language DML, I feel like this probably belongs on Stack Overflow. – jmite Apr 8 '16 at 20:58
• @jmite “Why was the language designed this way?” is a computer science question, though, and it's likely not to be well-received on SO (because the SO community mostly thinks that language design is a matter of whim, not science). Given that the basis for the question is a scientific question, I think this question is perfectly fine here. It would be better if it was more self-contained though: what are int and nat? Why does the use of <| matter? – Gilles 'SO- stop being evil' Apr 9 '16 at 13:08