1
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – jmite Apr 8 '16 at 20:58
  • 1
    $\begingroup$ @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? $\endgroup$ – Gilles Apr 9 '16 at 13:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.