A few questions on using linear types

[Brandon_Barker]

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

[Brandon_Barker]

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

[johann]

(*
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
)
| _ => ()

[Brandon_Barker]

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
)
| _ => ()

[gmhwxi]

You need

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

val y = grexp_to_string(!e2)

[gmhwxi]

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 = …

[Brandon_Barker]

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.

[Brandon_Barker]

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)

[gmhwxi]

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

[gmhwxi]

I just added linset_copy into linset_avltree. Thought that you may need it

[gmhwxi]

Also need to add

prval () = fold@ (e)

[Brandon_Barker]

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]

[gmhwxi]

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

[Brandon_Barker]

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)

[Brandon_Barker]

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)))

[Brandon_Barker]

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

[Chris_Double]

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

[gmhwxi]

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.

[Brandon_Barker]

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

[gmhwxi]

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