Re: [cap-talk] "Effect Capabilities for Haskell"

Thomas Leonard <[email protected]> Sat, 12 Dec 2015 13:23:24 +0000
Newsgroups gmane.comp.lang.e.general,gmane.comp.capabilities.general
Message-ID <CAG4opy9ZJ2AD-YiW8_vYQfWK6yNOued85OAWE5oN7A+baOFQmA@mail.gmail.com>
On 9 December 2015 at 05:19, Matt Rice <[email protected]> wrote:
> On Mon, Dec 7, 2015 at 8:12 PM, Mark S. Miller <[email protected]> wrote:
>> http://pleiad.dcc.uchile.cl/papers/2014/figueroaAl-sblp2014.pdf
>
> FWIW i've never managed to convince myself to learn haskell so, I
> don't get the emphasis on effects, when caps seem useful to me
> effect-free as well, i can't be certain that there isn't a effect-free
> capability and this is extending capabilities to effects as well, I do
> seem to recall a long thread about capabilities to immutable values in
> the past on list, but don't recall any concensus :)
>
> In the introduction it references sml's exceptions [6],
> I was made aware of this through Andreas Rossberg, when discussing
> Marc Stiegler's implementation of sealer/unsealers for Emily which
> used effects on boolean references,
>
> Attached is Andreas's makeSealer implementation for standard ML,
> including my attempts at explaining/breaking it, Ocaml implementation
> at the bottom of the email inline...
[...]
> Anyhow I had found this use of exceptions both surprising and
> non-obvious, and i hadn't seen or found any examples of it anywhere,
> the reference from the paper talks about it but doesn't provide examples.
> I've found searching for this particular usage of ML difficult due to
> the ubiquity of the
> terms involved, e.g. 'let polymorphism', 'polymorphic exceptions' ;)

I've seen this pattern referred to elsewhere as "universal types", as
it gives a form of dynamic typing, making sure you don't
(accidentally) get a value of the wrong type. Using exceptions was a
hack that used to be needed because only the exception type allowed
new variants to be added at runtime. More recent OCaml versions (e.g.
4.02) allow you to define your own open types. e.g.

type box = ..
module MakeSealer(X : sig type t end) = struct
  type box += Sealed of X.t
  let seal x = Sealed x
  let unseal = function
    | Sealed x -> Some x
    | _ -> None
end

(that's a literal ".." above, BTW)

Here's an example of it being used:

module A = MakeSealer(struct type t = int end)
module B = MakeSealer(struct type t = int end)

let show = function
  | None -> Printf.printf "None\n"
  | Some x -> Printf.printf "Some(%d)\n" x

let () =
  A.seal 1 |> A.unseal |> show;
  A.seal 2 |> B.unseal |> show;
  B.seal 3 |> B.unseal |> show

This prints:

Some(1)
None
Some(3)


-- 
Dr Thomas Leonard        http://roscidus.com/blog/
GPG: DA98 25AE CAD0 8975 7CDA  BD8E 0713 3F96 CA74 D8BA