Re: "Effect Capabilities for Haskell"

On Sat, Dec 12, 2015 at 5:23 AM, Thomas Leonard <[email protected]> wrote:
> 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.

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

> 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
> [email protected]
> http://www.eros-os.org/mailman/listinfo/cap-talk