dataviewtype

Dataviewtypes are linear analogues of datatypes. Due to potential complexity in type checking and proofs (as well as it being a concrete type) it is advised to make use of an [absviewtype] provide an interface for dataviewtypes.

A good introductory tutorial for dataviewtypes can be found here.

After reading the above tutorial, it may be useful to look at this highly illustrative example (source discussion):

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