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.
int
andnat
? Why does the use of<|
matter? $\endgroup$ – Gilles 'SO- stop being evil' Apr 9 '16 at 13:08