# How to use dependent types with the template system

**URL:** <https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412>\
**Category:** Google Group\
**Created:** [April 27, 2013, 10:29pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412 "2013-04-27T22:29:40Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [April 27, 2013, 10:29pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/1 "2013-04-27T22:29:40Z")

</div>

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]

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 27, 2013, 11:42pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/2 "2013-04-27T23:42:19Z")

</div>

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

…

assume gIdxMap\_vtype(n:int) = $LM.map(string, intBtw(0,n))

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [April 28, 2013, 1:57am UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/3 "2013-04-28T01:57:22Z")

</div>

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]

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 28, 2013, 2:16am UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/4 "2013-04-28T02:16:15Z")

</div>

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.  
\*)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 28, 2013, 8:28pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/5 "2013-04-28T20:28:03Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 28, 2013, 4:31am UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/6 "2013-04-28T04:31:52Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [April 28, 2013, 6:55pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/7 "2013-04-28T18:55:12Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [April 28, 2013, 2:56am UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/8 "2013-04-28T02:56:51Z")

</div>

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]

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [April 27, 2013, 11:43pm UTC](https://discourse.ats-lang.org/t/how-to-use-dependent-types-with-the-template-system/412/9 "2013-04-27T23:43:41Z")

</div>

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