# A few questions on using linear types

**URL:** <https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238>\
**Category:** Google Group\
**Created:** [February 28, 2013, 3:36am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238 "2013-02-28T03:36:04Z")\
**Posts on this page:** 20\
**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:** [February 28, 2013, 3:36am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/1 "2013-02-28T03:36:04Z")

</div>

This is my first time using linear types, so fair warning, it is going to  
be bad. I’m trying to integrate the use of sets into a boolean parser. The  
reasoning is that if you have an expression like (x and y and z and x),  
what you really want is just (x and y and z). When parsed, each literal’s  
string is assigned to a singleton set. Later on, an algorithm can be used  
to merge “neighboring” sets via union.

I have the following types:

viewdef genes = set(string)

dataviewtype GREXP =  
| GRgenes of genes  
| GRconj of (GREXP, GREXP)  
| GRdisj of (GREXP, GREXP)

_Question 1_: What is the right way to pass by reference in this situation  
(it seems a waste to be passing around entire sets by value)?:  
stringInOpIze (gset: &genes, inop: string): string

Using the “&” here results in:  
error(2): the function argument cannot be ascribed refval types.

_Question 2_: What might this error mean in the following code? I presume  
it has something to do with me not handling the consumption of s1 and s2.  
error(3): the linear dynamic variable [\_.view] needs to be consumed but it  
is preserved with the type [S2Eapp(S2Ecst(at\_viewt0ype\_addr\_view); S2Etop(1; S2Eapp(S2Ecst(set\_t0ype\_type); S2Ecst(string\_type))), S2Evar(\_(11041)))] instead.

fun grexp\_to\_string(e0: GREXP): string = case+ e0 of  
| GRconj (e1, e2) =\> let val epar = @(e1,e2) in case+ epar of  
| @(GRgenes (s1), GRgenes (s2)) =\> stringInOpIze(s1,“and”) + " and "

- stringInOpIze(s2,“and”)

Thanks,  
Brandon

---

<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:** [March 4, 2013, 5:55pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/2 "2013-03-04T17:55:38Z")

</div>

Thanks! … I just came to this conclusion about 1 minute ago as well, and  
hadn’t even checked yet.

---

<div class="post-metadata">

**Author:** ![johann](https://avatars.discourse-cdn.com/v4/letter/j/54ee81/32.png) [@johann](https://discourse.ats-lang.org/u/johann)\
**Post date:** [March 1, 2013, 5:14pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/3 "2013-03-01T17:14:36Z")

</div>

(\*  
Hello,  
inspired by the above question, I’ve cooked up an annotated example for  
dataviewtypes to illustrate the states of bindings (how/when certain  
bindings are usable/accessible) inside patterns. If I understand correctly,  
the general rule is, that whenever some binding x has been  
unfolded/deconstructed/matched by a pattern, it has to be fold@ed, to be  
accessible as x again. In case an “as” clause is used, e.g.  
case+ d0 of  
| dvt\_1 ( !d1 as dvt\_2(!d11,!d12) )

as below, !d1 is unfolded/deconstructed directly, and only  
accessible/usable as !d1 after fold@ing it again. As you see I’m having  
difficulty with the correct terminology for these state transitions, it  
might be helpful to come up with some kind of glossary for these things, to  
ease communication.

regards, Johann  
\*)

dataviewtype dvt =  
| dvt\_0 of ()  
| dvt\_1 of (dvt)  
| dvt\_2 of (dvt,dvt)

// (a)ccessible/usable  
// (u)nfolded  
// (f)olded  
// (n)o view available  
// (-) not in scope  
// d0 d1 d11  
d12 d121  
//  
fun use\_dvt(d0: !dvt):void = case+ d0 of // a - -

- 
  - 

```
| dvt_1 ( !d1 as dvt_2(!d11,!d12) ) => let // u u a   

```

a -  
val () = case+ (!d11,!d12) of //  
| (dvt\_0(), dvt\_1(!d121)) =\> let // u u u  
u a  
prval () = fold@ !d11 and () = fold@ !d12 // u u af  
af n  
in end //  
| (_,_) =\> () //  
prval () = fold@ !d1 // u af n  
n -  
prval () = fold@ d0 // af n n  
n -  
in end  
// d0 d1 d2  
d11 d12  
//  
| dvt\_2 ( !d1, !d2 ) =\> // u a a  
(case+ !d1 of  
| dvt\_2(!d11,!d12) =\> let // u u a a  
a  
prval () = fold@ !d1 // u af a n  
n  
prval () = fold@ d0 // af n n n  
n  
in end  
| \_ =\> fold@ d0  
)  
| \_ =\> ()

---

<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:** [August 6, 2014, 7:15pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/4 "2014-08-06T19:15:40Z")

</div>

Hi All,

In the process of updating the wiki, I wanted to update this example to  
work with ATS2, since it was helpful in understanding how  
to use dataviewtypes. As far as I can tell, the biggest difference seems to  
be that d1  
(in the first case) is always accessible, and apparently this wasn’t the  
case in ATS1 (though I haven’t double checked).  
Does this violate some notion of linearity with being able to access d1  
using multiple variables?

Is this due to a difference in how binding works using the ‘as’ keyword, or  
something else?

I also used $showtype to help understand these points, but I could still be  
in error.

dataviewtype dvt =  
| dvt\_0 of ()  
| dvt\_1 of (dvt)  
| dvt\_2 of (dvt,dvt)

// (a)ccessible/usable  
// (u)nfolded  
// (f)olded  
// (n)o view available  
// (-) not in scope  
// d0 d1 d11  
d12 d121  
//  
fun use\_dvt(d0: !dvt):void = case+ d0 of // a - - -  
| @dvt\_1 (d1 as dvt\_2(d11,d12) ) =\> let // u a a a  
val () = case+ (d11,d12) of //  
| (@dvt\_0 (), @dvt\_1 (d121) ) =\> let // u a u u  
a  
prval () = fold@ d11 and () = fold@ d12 // u a af af  
n  
in () end //  
| (_,_) =\> () //  
prval () = fold@ d0 // af n n n  
in () end // d0 d1 d2 d11  
d12

//------------------------  
| @dvt\_2 (d1,d2) =\> // u a a  
(case+ d1 of //  
| @dvt\_2 (d11,d12) =\> let // u u a a  
a  
prval () = fold@ d1 // u af a n  
n  
prval () = fold@ d0 // af n n n  
n  
in () end  
| \_ =\> fold@ d0  
)  
| \_ =\> ()On Friday, March 1, 2013 12:14:36 PM UTC-5, Johann Borck wrote:

> (\*  
> Hello,  
> inspired by the above question, I’ve cooked up an annotated example for  
> dataviewtypes to illustrate the states of bindings (how/when certain  
> bindings are usable/accessible) inside patterns. If I understand correctly,  
> the general rule is, that whenever some binding x has been  
> unfolded/deconstructed/matched by a pattern, it has to be fold@ed, to be  
> accessible as x again. In case an “as” clause is used, e.g.  
> case+ d0 of  
> | dvt\_1 ( !d1 as dvt\_2(!d11,!d12) )
> 
> as below, !d1 is unfolded/deconstructed directly, and only  
> accessible/usable as !d1 after fold@ing it again. As you see I’m having  
> difficulty with the correct terminology for these state transitions, it  
> might be helpful to come up with some kind of glossary for these things, to  
> ease communication.
> 
> regards, Johann  
> \*)
> 
> dataviewtype dvt =  
> | dvt\_0 of ()  
> | dvt\_1 of (dvt)  
> | dvt\_2 of (dvt,dvt)
> 
> ## // (a)ccessible/usable // (u)nfolded // (f)olded // (n)o view available // (-) not in scope // d0 d1 d11 d12 d121 //
> 
> fun use\_dvt(d0: !dvt):void = case+ d0 of // a - -
> 
> - 
> - 
> 
> ```
> | dvt_1 ( !d1 as dvt_2(!d11,!d12) ) => let // u u a   
> 
> ```
> 
> ## a - val () = case+ (!d11,!d12) of // | (dvt\_0(), dvt\_1(!d121)) =\> let // u u u u a prval () = fold@ !d11 and () = fold@ !d12 // u u af af n in end // | (_,_) =\> () // prval () = fold@ !d1 // u af n n - prval () = fold@ d0 // af n n n - in end // d0 d1 d2 d11 d12 //
> 
> ```
> | dvt_2 ( !d1, !d2 ) => // u a a
> (case+ !d1 of 
> | dvt_2(!d11,!d12) => let // u u a   
> 
> ```
> 
> a a  
> prval () = fold@ !d1 // u af a  
> n n  
> prval () = fold@ d0 // af n n  
> n n  
> in end  
> | \_ =\> fold@ d0  
> )  
> | \_ =\> ()

---

<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:** [March 1, 2013, 2:16am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/5 "2013-03-01T02:16:38Z")

</div>

You need

prval () = fold@ (!e2) _before_ the following line:

val y = grexp\_to\_string(!e2)

---

<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:** [February 28, 2013, 7:05pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/6 "2013-02-28T19:05:03Z")

</div>

First, you don’t need ‘epar’; you can just do 'case (e1, e1) of  
(GRgenes(s1), GRgenes(s2)) =\> …'  
Please add the following line

prval () = fold@ (e1) and () = fold@ (e2)

after

val x = …

---

<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:** [February 28, 2013, 5:26pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/7 "2013-02-28T17:26:41Z")

</div>

Note that there is a typo above in the commented out code:  
//fun stringInOpIze (gset: genes, inop:string): string  
should be:  
//fun stringInOpIze (gset: !genes, inop:string): string

Either way, the refval error occurs.

---

<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:** [March 4, 2013, 5:19pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/8 "2013-03-04T17:19:59Z")

</div>

I’ve encountered a new error while converting my last function to use the  
new dataviewtype:

dataviewtype GREXP =  
| GRgenes of genes  
| GRconj of genes  
| GRconj of (GREXP,GREXP)  
| GRdisj of genes  
| GRdisj of (GREXP,GREXP)

The function; red highlight is where there error occurs. I also wonder if  
declaring sequential vals is appropriate, or if it is better to use var  
(yellow highlight):  
fun toCNF (bexp: !GREXP): GREXP = let  
val LR = case+ bexp of  
| GRconj(!ex1,!ex2) =\> let  
val retv = (toCNF(!ex1),toCNF(!ex2))  
val \_ = $showtype retv  
prval () = fold@ bexp  
in retv end  
| GRdisj(ex1,ex2) =\> (toCNF(ex1),toCNF(ex2))  
| GRgenes(g) =\> (bexp, bexp) // ?  
in case+ bexp of  
| GRgenes(!g) =\> (fold@ bexp; bexp) //Start here  
| GRconj(!ex1,!ex2) =\> (case+ (LR.0,LR.1) of  
| (GRgenes(g1), GRgenes(g2)) =\> let  
var setu = linset\_union(!g1,!g2)  
val \_ = linset\_free(g1)  
val \_ = linset\_free(g2)  
in  
(fold@ bexp; GRconj setu)  
end  
| (_,_) =\> (fold@ bexp; GRconj(!ex1,!ex2))  
)  
| GRdisj(!ex1,!ex2) =\> (case+ (LR.0,LR.1) of  
// Handle disjunctive cases:  
| (GRdisj(lx1,lx2), GRdisj(rx1,rx2)) =\> let //GRdisj(LR.0,LR.1)  
val setu = linset\_union(!lx1,!lx2)  
val setu = linset\_union(setu,!rx1) //Any memory lost here?  
val setu = linset\_union(setu,!rx2)  
val \_ = linset\_free(lx1)  
val \_ = linset\_free(lx2)  
val \_ = linset\_free(rx1) //shouldn’t be able to free ?  
val \_ = linset\_free(rx2)  
in GRdisj setu end  
| (GRdisj(lx1,lx2), GRgenes(g)) =\> let //GRdisj(LR.0,!ex2)  
val setu = linset\_union(!lx1, !lx2)  
val setu = linset\_union(setu, g)  
val \_ = linset\_free(lx1)  
val \_ = linset\_free(lx2)  
val \_ = linset\_free(g)  
in GRdisj setu end  
| (GRgenes(g), GRdisj(rx1,rx2)) =\> let // GRdisj(!ex1,LR.1)  
val setu = linset\_union(!rx1, !rx2)  
val setu = linset\_union(setu, g)  
val \_ = linset\_free(rx1)  
val \_ = linset\_free(rx2)  
val \_ = linset\_free(g)  
in GRdisj setu end  
| (GRgenes(g1), GRgenes(g2)) =\> let  
var setu = linset\_union(!g1,!g2)  
val \_ = linset\_free(g1)  
val \_ = linset\_free(g2)  
in  
GRdisj setu  
end  
// Distribute OR over ANDs:  
| (GRconj(lx1,lx2),GRconj(rx1,rx2)) =\>  
GRconj(GRconj(GRconj(toCNF(GRdisj(lx1,rx1)),toCNF(GRdisj(lx2,rx1))),  
toCNF(GRdisj(lx1,rx2))),toCNF(GRdisj(lx2,rx2)))  
// Handle e.g.: (… OR …) OR (… AND …)  
| (GRconj(lx1,lx2), _) =\>  
GRconj(toCNF(GRdisj(lx1,LR.1)),toCNF(GRdisj(lx2,LR.1)))  
| (_ ,GRconj(rx1,rx2)) =\>  
GRconj(toCNF(GRdisj(LR.0,rx1)),toCNF(GRdisj(LR.0,rx2)))  
)  
end

And the error (I’m not sure what lower bound means here):

**SHOWTYPE** (/media/RAID5/share/ATS\_learning/toCNF3.dats: 11274(line=428,  
offs=27) – 11278(line=428, offs=31)): S2Etyrec(flt; 0; 0=S2Ecst(GREXP),  
1=S2Ecst(GREXP))  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 11320(line=430, offs=12) –  
11324(line=430, offs=16): error(3): sort mismatch: the sort of [s2V(3185)]  
is [t@ype], but the sort of its lower bound is [viewt@ype].  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 11320(line=430, offs=12) –  
11324(line=430, offs=16): error(3): mismatch of static terms (tyleq):  
The needed term is: S2EVar(3185)  
The actual term is: S2Etyrec(flt; 0; 0=S2Ecst(GREXP), 1=S2Ecst(GREXP))  
exit(ATS): uncaught exception:  
\_2fhome\_2ffac2\_2fhwxi\_2fresearch\_2fATS\_2fIMPLEMENT\_2fGeizella\_2fAnairiats\_2fsvn\_2fats\_2dlang\_2fsrc\_2fats\_error\_2esats\_\_FatalErrorException(1233)

---

<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:** [March 3, 2013, 4:41am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/9 "2013-03-03T04:41:04Z")

</div>

(\*  
First, opt (a, b)? and a? are really just the same  
\*)

(\*  
Here is a typical sequence of using linset\_choose:  
\*)

var gene: string // uninitialized  
val ans = linset\_choose(!s, gene)  
val () = assertloc (ans) // [linset\_choose] succeeded  
prval () = opt\_unsome {string} (gene)  
// now [gene] contains a value of the type [string]

(\*  
Note that the [linset] package should primarily be used to implement  
abstract types.  
\*)

---

<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:** [March 4, 2013, 5:53pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/10 "2013-03-04T17:53:34Z")

</div>

I just added linset\_copy into linset\_avltree. Thought that you may need it  
🙂

---

<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:** [February 28, 2013, 7:05pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/11 "2013-02-28T19:05:56Z")

</div>

Also need to add

prval () = fold@ (e)

---

<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:** [March 5, 2013, 10:25pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/12 "2013-03-05T22:25:32Z")

</div>

Pretty trivial but here is my try  
implement{a}  
linset\_choose  
(xs, x0) = case+ xs of  
| list\_vt\_cons (x, !p\_xs) =\> let  
prval () = fold@ xs  
val () = x0 := x  
prval () = opt\_some {a} (x0)  
in  
true  
end // end of [list\_vt\_cons]  
| list\_vt\_nil () =\> let  
prval () = fold@ xs  
prval () = opt\_none {a} (x0)  
in  
false  
end // end of [list\_vt\_nil]  
// end of [linset\_choose]

---

<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:** [March 5, 2013, 10:41pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/13 "2013-03-05T22:41:08Z")

</div>

It is implemented. You need to have the following lines

staload = "libats/SATS/linset\_avltree.sats"  
staload \_ = “libats/DATS/linset\_avltree.dats” // I think this one is missing

---

<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:** [March 5, 2013, 7:04pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/14 "2013-03-05T19:04:14Z")

</div>

It all typechecks! If it works as expected, it will be pretty amazing;  
certainly the typechecker & flymake have already kept me from doing many  
stupid things.

Unfortunately, I’ve been unable to compile it. It seems that no matter  
which combination of the following I use I am stuck with an error:

staload "libats/SATS/linset\_listord.sats"  
staload \_ = "libats/DATS/linset\_listord.dats"  
dynload “libats/DATS/linset\_listord.dats”

brandon@gulab:/media/RAID5/share/ATS\_learning$ atscc -o toCNF3 toCNF3.dats  
sstream.dats sstream.sats  
/media/RAID5/share/ATS\_learning/ats-lang-anairiats-0.2.9/bin/atsopt  
–output toCNF3\_dats.c --dynamic toCNF3.dats  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 2191(line=104, offs=13) –  
2202(line=104, offs=24): error(ccomp): the template definition for  
[linset\_copy] is unavailable at [linset\_copy$1987\_ats\_ptr\_type].  
exit(ATS): uncaught exception:  
\_2fhome\_2ffac2\_2fhwxi\_2fresearch\_2fATS\_2fIMPLEMENT\_2fGeizella\_2fAnairiats\_2fsvn\_2fats\_2dlang\_2fsrc\_2fats\_error\_2esats\_\_FatalErrorException(1233)  
brandon@gulab:/media/RAID5/share/ATS\_learning$ tmux attach  
[detached]  
brandon@gulab:/media/RAID5/share/ATS\_learning$ atscc -o toCNF3 toCNF3.dats  
sstream.dats sstream.sats  
/media/RAID5/share/ATS\_learning/ats-lang-anairiats-0.2.9/bin/atsopt  
–output toCNF3\_dats.c --dynamic toCNF3.dats  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 8272(line=312, offs=17) –  
8285(line=312, offs=30): error(ccomp): the template definition for  
[linset\_choose] is unavailable at [linset\_choose$1991\_ats\_ptr\_type].  
exit(ATS): uncaught exception:  
\_2fhome\_2ffac2\_2fhwxi\_2fresearch\_2fATS\_2fIMPLEMENT\_2fGeizella\_2fAnairiats\_2fsvn\_2fats\_2dlang\_2fsrc\_2fats\_error\_2esats\_\_FatalErrorException(1233)  
brandon@gulab:/media/RAID5/share/ATS\_learning$ tmux attach  
[detached]  
brandon@gulab:/media/RAID5/share/ATS\_learning$ atscc -o toCNF3 toCNF3.dats  
sstream.dats sstream.sats  
/media/RAID5/share/ATS\_learning/ats-lang-anairiats-0.2.9/bin/atsopt  
–output toCNF3\_dats.c --dynamic toCNF3.dats  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 1520(line=61, offs=17) –  
1523(line=61, offs=20): error(2): unrecognized static identifier [set].  
exit(ATS): uncaught exception:  
\_2fhome\_2ffac2\_2fhwxi\_2fresearch\_2fATS\_2fIMPLEMENT\_2fGeizella\_2fAnairiats\_2fsvn\_2fats\_2dlang\_2fsrc\_2fats\_error\_2esats\_\_FatalErrorException(1233)

---

<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:** [February 28, 2013, 6:48pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/15 "2013-02-28T18:48:43Z")

</div>

You are right that dataviewtypes can be difficult, but I am not sure about  
how to use a reference-counted absviewtype in this context. I’ve  
highlighted the part of the function I have attempted to change, and the  
errors below. I do not have much code that needs to talk to the GREXP other  
than this (just one other similar function), so perhaps it is reasonable to  
keep as a dataviewtype for now? I have tried a few things, none very  
fruitful. I will continue to try.

fun print\_pretty\_grexp (grexp: !GREXP): void = () where {  
(\* Idea is to put parentheses around a sequence  
of disjunctions, to improve the ease of identifying  
conjunctions and disjunctions, and improve readability in general. \*)

fun grexp\_to\_string(e0: !GREXP): string = case+ e0 of  
| GRconj (e1, e2) =\> let val epar = @(e1,e2) in case+ epar of  
| @(GRgenes (s1), GRgenes (s2)) =\> let  
val \_ = $showtype e0  
val x = stringInOpIze(s1,“and”) + " and " + stringInOpIze(s2,“and”)  
in x end (\*Somehow type error shows up here, though this should be  
a string \*)  
| @(~GRgenes (s1), GRconj (_,_)) =\> let val x =  
stringInOpIze(s1,“and”) + " and " + grexp\_to\_string(e2)  
in (linset\_free(s1); x) end  
| @(GRconj (_,_), GRgenes (s2)) =\> grexp\_to\_string(e1) + " and " +  
stringInOpIze(s2,“and”)  
| @(GRconj (_,_), GRconj (_,_)) =\> grexp\_to\_string(e1) + " and " +  
grexp\_to\_string(e2)  
| @(GRdisj (_,_), GRdisj (_,_)) =\> “(” + grexp\_to\_string(e1) + “) and  
(” + grexp\_to\_string(e2) + “)”  
| @(e1, GRdisj (_,_)) =\> grexp\_to\_string(e1) + " and (" +  
grexp\_to\_string(e2) + “)”  
| @(GRdisj (_,_), e2) =\> “(” + grexp\_to\_string(e1) + ") and " +  
grexp\_to\_string(e2)  
end  
| GRdisj (e1, e2) =\> let val epar = @(e1,e2) in case+ epar of  
| @(GRgenes (s1), GRgenes (s2)) =\> stringInOpIze(s1,“or”) + " or " +  
stringInOpIze(s2,“or”)  
| @(GRgenes (s1), GREXP) =\> stringInOpIze(s1,“or”) + " or " +  
grexp\_to\_string(e2)  
| @(GREXP, GRgenes (s2)) =\> grexp\_to\_string(e1) + " or " +  
stringInOpIze(s2,“or”)  
| \_ =\> grexp\_to\_string(e1) + " or " + grexp\_to\_string(e2)  
end  
| GRgenes (e1) =\> ($raise InvalidCase; ())  
val grstr = grexp\_to\_string(grexp)  
val grstr = grstr + "\n"  
val \_ = print(grstr)  
}

The error:  
_atscc -tc /media/RAID5/share/ATS\_learning/toCNF3.dats_  
_/media/RAID5/share/ATS\_learning/ats-lang-anairiats-0.2.9/bin/atsopt  
–typecheck --dynamic /media/RAID5/share/ATS\_learning/toCNF3.dats_  
_ **SHOWTYPE** (/media/RAID5/share/ATS\_learning/toCNF3.dats: 4749(line=212,  
offs=27) – 4751(line=212, offs=29)): S2Edatconptr(GRconj;  
S2Evar((11039)), S2Evar((11040)))_  
_/media/RAID5/share/ATS\_learning/toCNF3.dats: 4840(line=214, offs=12) –  
4841(line=214, offs=13): error(3): mismatch of static terms (tyleq):_  
_The needed term is: S2Ecst(GREXP)_  
_The actual term is: S2Edatconptr(GRconj; S2Evar((11039)),  
S2Evar((11040)))_

---

<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:** [March 5, 2013, 9:53pm UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/16 "2013-03-05T21:53:31Z")

</div>

Looks like linset\_choose wasn’t implemented in the ordered list version,  
maybe I can work on adding it in. Also, sorry if I wasn’t clear earlier  
about linset\_avltree. I knew which file it would be in, I just didn’t know  
where to find the updated file specifically online (or if it was even  
uploaded yet).

---

<div class="post-metadata">

**Author:** ![Chris\_Double](https://avatars.discourse-cdn.com/v4/letter/c/e19b73/32.png) [@Chris\_Double](https://discourse.ats-lang.org/u/Chris_Double)\
**Post date:** [February 28, 2013, 3:52am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/17 "2013-02-28T03:52:03Z")

</div>

> _Question 1_: What is the right way to pass by reference in this  
> situation (it seems a waste to be passing around entire sets by value)?:  
> stringInOpIze (gset: &genes, inop: string): string

They are already passed around as pointer’s, not the entire datastructure  
by value, so this is fine:

stringInOpIze (gst: genes, inopt: string): string

or this if you don’t want to consume the linear type:

stringInOpIze (gst: !genes, inopt: string): string

> _Question 2_: What might this error mean in the following code? I presume  
> it has something to do with me not handling the consumption of s1 and s2.  
> error(3): the linear dynamic variable [\_.view] needs to be consumed but it  
> is preserved with the type [S2Eapp(S2Ecst(at\_viewt0ype\_addr\_view); S2Etop(1; S2Eapp(S2Ecst(set\_t0ype\_type); S2Ecst(string\_type))), S2Evar(\_(11041)))] instead.

Yes, the error is to do with consuming the linear types. Your definition of  
‘grexp\_to\_string’ consumes ‘e0’ (use “e0: !GREXP” to not do this).  
Assuming you do want to consume it you can add a “~” to the pattern to  
automatically do this but you’ll still have to make sure all the relevant  
case branches correctly consume it:

case+ e0 of  
| ~GRconj( …)

I cover some of this in an example here which might help you track down  
where the problem is:  
[http://www.bluishcoder.co.nz/2011/02/27/linear-datatypes-in-ats.html](http://www.bluishcoder.co.nz/2011/02/27/linear-datatypes-in-ats.html)

---

<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:** [March 3, 2013, 4:42am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/18 "2013-03-03T04:42:35Z")

</div>

> > Also, what is the difference in pfg and pf, above?

pf is the proof that allows you to use the memory.  
pfg is the proof that allows you to free the memory.

---

<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:** [March 3, 2013, 4:02am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/19 "2013-03-03T04:02:08Z")

</div>

Thanks Hongwei & Johann,

That’s a great demo! I was able to work through the rest of the function  
without problems, except in the last case where I need to call  
linset\_choose:

// HX: choose an element in an unspecified manner  
//  
fun{a:t@ype}  
linset\_choose (  
xs: !set a, x: &a? \>\> opt (a, b)  
) : #[b:bool] bool (b) // end of [linset\_choose]

I feel that I somewhat begin to understand “x: &a? \>\> opt (a, b)”, but I  
may still be very far from the mark; I think it means something like the  
following: x is an address that is unitialized of type a, and after  
initialization it contains opt(a). Now this does not make sense to me: why  
must the type change of “a” to “option(a)” - why wouldn’t it just be: “x: opt  
(a, b)? \>\> opt (a, b)”?

Much like the imprecise reasoning above, I have written some imprecise code:  
val (pfg, pf | gene) = ptr\_alloc ()  
val \_ = $showtype !gene  
val found = if ssize \<\> 1  
then ($raise InvalidCase; linset\_choose(!s,!gene ))  
else linset\_choose(!s,gene)  
prval () = fold@ e0  
in gene end

**SHOWTYPE** (/media/RAID5/share/ATS\_learning/toCNF3.dats: 7183(line=275,  
offs=26) – 7188(line=275, offs=31)): S2Etop(0; S2Ecst(string))  
/media/RAID5/share/ATS\_learning/toCNF3.dats: 7277(line=277, offs=50) –  
7282(line=277, offs=55): error(3): mismatch of static terms (tyleq):  
The needed term is: S2Etop(0; S2EVar(3165))  
The actual term is: S2Etop(0; S2Ecst(string\_type))

So I think I have the “S2Etop(0;” part right: this is an unitialized value.  
But what could S2EVar(3165) be?

Also, what is the difference in pfg and pf, above?

Hongwei, I will implement abstract types more someday, but possibly not in  
this project as it is nearly finished (I think).

---

<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:** [February 28, 2013, 4:07am UTC](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238/20 "2013-02-28T04:07:34Z")

</div>

Above all, I must say that using dataviewtypes (linear datatypes) can be  
quite difficult.

Declaring GREXP as a dataviewtype can easily get you into a situation where  
all you do  
is to fight the typechecker.

If you really want a linear GREXP, try to make it a reference-counted  
absviewtype.

–Hongwei

[Next page](https://discourse.ats-lang.org/t/a-few-questions-on-using-linear-types/238.md?page=2)