How to use dependent types with the template system

Google Group
1

Here’s an example where I want to create a map with integer values only
within a certain range. Is this a crazy thing to do? I’m also not sure if
this is something best left to ATS2.

Firstly, it appears I’m not sure how to create a “new” dependent type
(highlighted in yellow):

absviewtype gIdxMap
typedef gIdxMap (n:int) = gIdxMap n

extern
fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(0,n) i

extern
fun gIdxMap_free(mp: gIdxMap):<> void

extern
fun gIdxMap_insert {i,n:nat | i < n} (mp: &gIdxMap n, gene: string, ival:
intBtw(0,n) i
):<> bool

extern
fun gIdxMap_make_nil(): gIdxMap

local

staload LM = "libats/SATS/linmap_avltree.sats"
staload _ = "libats/DATS/linmap_avltree.dats"
assume gIdxMap = {n:nat} $LM.map(string, intBtw(0,n))

in // in of [local]

implement
gIdxMap_make_nil() = $LM.linmap_make_nil {string, int} ()

implement
gIdxMap_find {n:nat} (mp n, k): intBtw(0,n) i = let
var res: int?
val b = $LM.linmap_search (mp, k, lam(x,y)
=> compare_string_string(x,y), res)
in
if b then let
prval () = opt_unsome {int} (res)
in res end
else let
prval () = opt_unnone {int} (res)
in ( (* print(k + “not found\n”); $raise MapKeyNotFound;*) ~1.0) end
end // end of [gIdxMap_find]

implement
gIdxMap_free(mp) = $LM.linmap_free(mp)

implement
gIdxMap_insert (mp n,gene, ival i) = let
var rdval: int?
val b = $LM.linmap_insert<string,int>
(mp, gene, dval, lam(x,y) => compare_string_string(x,y),rdval)
//How does this work?:
prval () = opt_clear (rdval)
in b end

end // end of [local]

2

absviewtype gIdxMap_vtype (n:int)
typedef gIdxMap (n: int) = gIdxMap_vtype (n)

…

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(0,n))

3

Thanks; I used viewdef instead of typedef and that part typechecked. Things
are getting a bit tricky when it comes to separating a function definition
from its implementation (highlighted). I’d like the static variables
associated to function arguments available in the implementation, but “the
function argument cannot be ascribed refval types.” I could probably hack a
way around this using prfuns, but I’m betting there’s a more elegant way.

absviewtype gIdxMap_vtype (n:int)
viewdef gIdxMap (n: int) = gIdxMap_vtype (n)

extern
fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(~1,n)

extern
fun gIdxMap_free {n:nat} (mp: gIdxMap n):<> void

extern
fun gIdxMap_insert {n:nat} (mp: &gIdxMap n, gene: string, ival: intBtw(~1,n)
):<> bool

extern
fun gIdxMap_make_nil {n:nat} (n:int n): gIdxMap n

local

staload LM = "libats/SATS/linmap_avltree.sats"
staload _ = “libats/DATS/linmap_avltree.dats”

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(~1,n))

in // in of [local]

implement
gIdxMap_make_nil {n:int} (n:int n) =
$LM.linmap_make_nil {string, intBtw(~1,n)} ()

implement
gIdxMap_find {n:int} (mp: &gIdxMap n , k) = let
var res: intBtw(~1,n)
val b = $LM.linmap_search (mp, k, lam(x,y)
=> compare_string_string(x,y), res)
in
if b then let
prval () = opt_unsome {Int} (res)
in res end
else let
prval () = opt_unnone {Int} (res)
in ( (* print(k + “not found\n”); $raise MapKeyNotFound;*) ~1) end
end // end of [gIdxMap_find]

implement
gIdxMap_free(mp) = $LM.linmap_free(mp)

implement
gIdxMap_insert (mp, gene, ival) = let
var rdval: int?
val b = $LM.linmap_insert<string,Int>(mp, gene, ival, lam(x,y)
=> compare_string_string(x,y),rdval)
//How does this work?:
prval () = opt_clear (rdval)
in b end

end // end of [local]

4

viewdef -> viewtypedef

implement
gIdxMap_find {n:int} (mp: &gIdxMap n , k) = let

changes to

implement
gIdxMap_find {n} (mp, k) = let
(*
the static ‘n’ is available here.
*)

5

Writing something like

fun loop (…): void = …

does NOT mean that a closure is to be created for loop. It simply means
that variables from outside can be used in the body of loop.

6

The comparison should be moved out. Otherwise, it gets created whenever
gIdxMap_insert is called.

local

val cmp = lam(x:string,y:string):int = compare (x, y)

in

…

end

7

Is this advice specific to closures? I often see functions (e.g. fun
loop(…)) defined inside of other functions.

8

Great, I attach a type checking (but untested) version for completeness.
The find function returns a negative 1 if a value is not found in the map,
which should probably be changed to used the Option mechanism.
absviewtype gIdxMap_vtype (n:int)
viewdef gIdxMap (n: int) = gIdxMap_vtype (n)

extern
fun gIdxMap_find {n:nat} (mp: &gIdxMap n, k: string): intBtw(~1,n)

extern
fun gIdxMap_free {n:nat} (mp: gIdxMap n):<> void

extern
fun gIdxMap_insert {n:nat} (mp: &gIdxMap n, gene: string, ival: intBtw(~1,n)
):<> bool

extern
fun gIdxMap_make_nil {n:nat} (n:int n): gIdxMap n

local

staload LM = "libats/SATS/linmap_avltree.sats"
staload _ = “libats/DATS/linmap_avltree.dats”

assume gIdxMap_vtype(n:int) = $LM.map(string, intBtw(~1,n))

in // in of [local]

implement
gIdxMap_make_nil {n:int} (n:int n) =
$LM.linmap_make_nil {string, intBtw(~1,n)} ()

implement
gIdxMap_find {n} (mp, k) = let
var res: intBtw(~1,n)?
val b = $LM.linmap_search (mp, k, lam(x,y)
=> compare_string_string(x,y), res)
in
if b then let
prval () = opt_unsome {intBtw(~1,n)} (res)
in res end
else let
prval () = opt_unnone {intBtw(~1,n)} (res)
in ( (* print(k + “not found\n”); $raise MapKeyNotFound; *) ~1) end
end // end of [gIdxMap_find]

implement
gIdxMap_free(mp) = $LM.linmap_free(mp)

implement
gIdxMap_insert {n} (mp, gene, ival) = let var rdval: intBtw(~1,n)?
val b = $LM.linmap_insert<string, intBtw(~1,n)>(mp, gene, ival, lam(x,y)
=> compare_string_string(x,y),rdval)
//How does this work?:
prval () = opt_clear (rdval)
in b end

end // end of [local]

9

‘intBtw(0, n) i’ is wrong; it should just be ‘intBtw(0, n)’.