[cap-talk] "Effect Capabilities for Haskell"

[Mark S. Miller]

http://pleiad.dcc.uchile.cl/papers/2014/figueroaAl-sblp2014.pdf

--

    Cheers,
    --MarkM

[Matt Rice]

On Mon, Dec 7, 2015 at 8:12 PM, Mark S. Miller <eri...@google.com> 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...

The condensed compiler output from SML/nj of various runsj:

val makeSealer = fn : unit -> ('a -> exn) * (exn -> 'a)
datatype Mode = BadUnseal | GoodUnseal | RaiseSealed
val foo = fn : 'a * Mode -> 'a * 'a
val a = ("secret1","secret1") : string * string
val b = ("?","?") : string * string
val c = ("??","??") : string * string
val bar = fn : string -> exn * (exn -> string)
val d = "secret6..." : string

uncaught exception Seal
raised at: mkseal.sml:18.43-18.50
/bin/sml: Fatal error -- Uncaught exception Seal with "secret4" raised at ...

uncaught exception Seal
raised at: mkseal.sml:18.43-18.50
/bin/sml: Fatal error -- Uncaught exception Seal with <unknown> raised at ...

uncaught exception Seal
raised at: mkseal.sml:91.14-91.16
/bin/sml: Fatal error -- Uncaught exception Seal with "secret7" raised at ...

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

The issue with the top-level exception was with the SML/NJ compiler,
the other compiler I tested with, mlton produces just "unhandled
exception: Seal" which seems acceptable

the reference states that this is a property of SML exceptions but not
ocaml ones,
the ocaml variation mentioned earlier, it appears to get the same
behaviour through the combination of modules and exceptions, I haven't
tested this one to the same extent (e.g. mixing calls to instances of
sealers/unsealer modules which share the same type) though...
apologies for the wall of text.

module type SEALED =
sig
type t
val seal : t -> exn
val unseal : exn -> t
end

module MakeSealer (X : sig type t end) : SEALED with type t = X.t =
struct
type t = X.t
exception Seal of t
let seal x = Seal x
let unseal = function Seal x -> x | _ -> failwith "unseal"
end

module S = MakeSealer (struct type t = int end)
let n = S.unseal (S.seal 7)

[Thomas Leonard]

On 9 December 2015 at 05:19, Matt Rice <rat...@gmail.com> wrote:
> On Mon, Dec 7, 2015 at 8:12 PM, Mark S. Miller <eri...@google.com> 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
_______________________________________________
cap-talk mailing list
cap-...@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk

[Matt Rice]

Thanks,

I believe that in 1ml it has no particular name again,
in particular it's just a functor which returns some abstract type
value (sealed in the example below)

and from there you can use the normal environment scoping mechanisms
for values to hide the type value, which doesn't impact your ability
to hold values of that type.

not that i'm particularly confident in my understanding of the language,
but it seems to make sense and appears to work

type SEAL a = {
type sealed
;; Here have an alias.
;type unsealed = a
;seal : a -> sealed
;unseal : sealed -> a
};

Seal a :> SEAL a = {
type sealed = a
;type unsealed = a
;seal x = x
;unseal x = x
};

local
SealedInt = Seal int
;S2 = Seal int
in
;; For reasons, you may have -x but not x
enjoy = fun (func, s) => func(SealedInt.unseal(s) * (0 - 1))
;s = SealedInt.seal 5
;s2 = S2.seal 2
end;

foo = enjoy(fun v => v + 1, s);
;; type error... can't do anything with s2 but pass it around
;; foo = enjoy(fun v => v + 1, s2);
_ = Int.print(foo);

> Using exceptions was a
> hack that used to be needed because only the exception type allowed
> new variants to be added at runtime.

Indeed