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

[Chris Double]

On Thursday, February 28, 2013 4:36:04 PM UTC+13, Brandon Barker wrote:

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]

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

[Brandon Barker]

Thanks, the blog was pretty helpful. Interestingly, when I try using extern, I get the same type of error:

extern

fun stringInOpIze (gset: genes, inop:string): string

implement 

stringInOpIze (gset: !genes, inop: string): string = let

1264(line=56, offs=15) -- 1292(line=56, offs=43): error(2): the function argument cannot be ascribed refval types.

A full example with working type-checked code (I continue to consider your and Hongwei's advice):

staload _(*anon*) = "libc/SATS/stdio.sats"

//

staload _(*anon*) = "prelude/DATS/array.dats"

staload _(*anon*) = "prelude/DATS/array0.dats"

//

staload _(*anon*) = "prelude/DATS/list.dats"

staload _(*anon*) = "prelude/DATS/list0.dats"

staload _(*anon*) = "prelude/DATS/list_vt.dats"

//

staload _(*anon*) = "prelude/DATS/matrix.dats"

staload _(*anon*) = "prelude/DATS/matrix0.dats"

//

staload _(*anon*) = "prelude/DATS/option.dats"

staload _(*anon*) = "prelude/DATS/option0.dats"

//

staload _(*anon*) = "prelude/DATS/pointer.dats"

//

staload _(*anon*) = "prelude/DATS/reference.dats"

//

(* ********************************* Begin CODE ******************************** *)

staload "prelude/SATS/string.sats"

staload "prelude/SATS/filebas.sats"

staload "prelude/SATS/printf.sats"

staload "libc/SATS/stdio.sats"

staload "prelude/SATS/integer.sats"

staload "prelude/SATS/list.sats"

staload "libats/SATS/linset_avltree.sats"   

staload _ = "libats/DATS/linset_avltree.dats"   

staload "sstream.sats"

dynload "sstream.dats"

#define NUL '\000'

viewdef genes = set(string)

dataviewtype GREXP = 

  | GRgenes of genes

  | GRconj of (GREXP, GREXP)

  | GRdisj of (GREXP, GREXP)

//extern

//fun stringInOpIze (gset: genes, inop:string): string

//implement 

fun stringInOpIze (gset: !genes, inop: string): string = let

    val glist:List(string) = list_of_list_vt(linset_listize (gset))

    fun loop(astr:string, alist:List(string)): string = case+ alist of

      | list_nil () => ""

      | list_cons(x,xs) => loop(astr + " " + inop + " " + x, xs )

  in       

    loop("",glist)    

  end

[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]

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

[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 = ....

[gmhwxi]

Also need to add

prval () = fold@ (e)

[Brandon Barker]

Thanks, I also talked to Chris quite a bit about this one.

With his help I got through the first case ok. It is in blue below. 

The second case needs to make use of e2 in addition to s1 and s2, which seems to be where the problem is happening (red below).

We tried a few things for case 2 (e.g. "s2 as GRconj(_,_)" as the second pattern), and noticed case 2 would typecheck if we simply left out GRconj(_,_) and in its place had just _. This is where we got stuck.

I attached the file as well.

//implement

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) => (case+ (!e1, !e2) of 

      | (GRgenes (!s1), GRgenes (!s2)) => let 

        val _ = $showtype e0 

        val x = stringInOpIze(!s1,"and") + " and " + stringInOpIze(!s2,"and")

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

        in x end

      | (GRgenes (!s1), GRconj(_,_)) => let

        val x = stringInOpIze(!s1,"and") + " and " 

        val y = grexp_to_string(!e2)        

        prval () = fold@ !e1 

        prval () = fold@ e0

        in x + y end

[gmhwxi]

You need

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

val y = grexp_to_string(!e2)



[gmhwxi]

By the way, using concrete types like set(string) should be avoided in general.
Try to introduce an abstract (view)type for it.

[johann...@densedata.com]

(*
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]

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

      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]

(*
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]

>> 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, I believe I was getting in trouble with dependent types again with the if/else (!gene typo aside in the above paste). Silly thing to do, I should stick to watching movies at night.

[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]

You need a type annotation:

val LR = (case+ ... of ...): (GREXP, GREXP)

[gmhwxi]

Note that linset_union actually consumes its two arguments.

[gmhwxi]

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

[Brandon Barker]

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

[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]

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

[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]

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

[gmhwxi]

I think the example is a bit too complex.

Here is a clarifying example:

datavtype dvt =
  | dvt0 of ()
  | dvt2 of (dvt,dvt)

fun foo (x: !dvt): void =
  case+ x of
  | dvt0 () => ()
  | dvt2 (x1, x2) => () // x1 and x2 are values
  | @dvt2 (x1, x2) => fold@(x) // x1 and x2 are l-values

Basically, you need to put @ in front of a linear constructor if you want to
use the arguments of the constructor as l-values. Why l-values? Because
an l-value allows its content to be modified. Note that explicit folding (fold@)
is needed if @ is used.

[Brandon Barker]

OK, great - intuitively this make a lot of sense. I added it here: https://sourceforge.net/p/ats2-lang/wiki/dataviewtype/

Brandon Barker
brandon...@gmail.com

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3a97996d-313c-40bb-ac08-40e262e201d7%40googlegroups.com.