[HARD] map on slot data contents

[keigoi]

Usual pattern is

let f s = 
  match%lin get s with
  | Cons(x,#s) ->

This pattern uses s twice and is type error: first s has ('a linlist_ lin, empty, 'a,'b) slot while second has (empty, 'linlist_ lin, 'b, 'a) slot.

Some "map" on data contents in a slot would be nice

[keigoi]

val map: ('a data lin, 'b data lin, 'pre, 'post) slot -> ('a -> 'b * c) -> ('pre, 'post, 'c) monad

would work?

[keigoi]

This suffices for multiparty.ml but doesn't work for linlist.ml case (slot content has both Data and Lin).

match%lin doesn't work neither since:

match%lin (expr1: (?,?,'a linlist_ lin) lin_match) with
| Cons(x,#s) ->  expr2
==>
expr1 >>= function
| Cons(x, _pat) ->  set s pat (* here s is empty->'a linlist_ lin *) >> expr2

(In mutiparty.ml we can hide data part in "'a data" within a signature and ensure that data content is linearly accessed by outside.)

[keigoi]

Assume %linget and %linmap:

let rec map f s =
  match%linget s with
  | x::#s -> 
    map f s >> 
    [%linmap f x:: !!s]
  | [] -> return ()

which translates to:

let rec map f s =
  Internal.peek__ s >>= function
    | x::_newpat_ -> 
      Internal.force_put__ _newpat_ >> 
      map f s >> 
      Internal.peek__ s >>= fun _newpat2_ ->
      Internal.force_put__ (f x::_newpat2_)
    | [] -> Internal.force_put__ s [] >> return ()

It seems that each peek/force_put pair treats things linearly.
However, inserting force_put__ at [] case can be confusing.

Another caveat could be that pattern sometimes do not contain same s:

  match%linget s with
  | x::#t -> (* bad *)

For iter, it changes list to empty so it requires two lens at least, anyway.

[keigoi]

Also, we must check for linear occurrences of lens for %linget and %linmap.

Names are also confusing. There already is %lin and %linval (and functions lin and lin_).

let%linget x::#s = s in ... (* they must be the same lens *)

let%lin x::#t = get s in ... (* they can differ *)

match%linget s with
| x::#s -> ...

match%lin get s with
| x::#t -> ...

let%lin #t = [%linval Cons(f x, !! s)] in return ()

[%linmap Cons(f x, %s)]

• lin_match is returned by get and [%linval ..] (I sometimes forget the latter)

• Two flavour of slot setters:

set s Nil

let%lin #s = [%linval Nil] in return ()

And %linget and %linmap are actually "advanced" features, since it is not necessary for first-order slot programming.

• It seems that Linocaml.map can not be simulated by %linget nor %linmap.

[keigoi]

Writers of rev_map would suffer from obfuscation at [] case:

let rev_map f s =
  let rec loop () =
    match%linget s with
    | Cons(x,#s) -> [%linmap Cons(f x,#t)] >>= loop
    | Nil -> set s Empty???
  in
  set t Nil >>
  get t (loop ())

It is better to require some annotataion for Nil case to make explicit the fact that Nil is stored at s again.

We want to write

| Nil as #s

However this results in syntax error since #s is not a variable but a constructor pattern in OCaml.

| Nil [@@ #s]

is possible?