Re: cap patterns in 1ml

On Mon, Jan 25, 2016 at 12:19 PM, Raoul Duke <[email protected]> wrote:
> On Sun, Jan 24, 2016 at 1:48 PM, Matt Rice <[email protected]> wrote:
>> On Tue, Jan 19, 2016 at 7:45 PM, Matt Rice <[email protected]> wrote:
>>> I haven't quite gotten to factories yet,
>> Well I am skeptical that types & pure constructors alone is going to
>> be able to confine now primarily because I don't believe the effects
>> of a monad within in a pure constructor are going to be confined to
>> the pure constructor, without some form of environment restriction
>> e.g. the usual ways
>
>
> Is there a good example anywhere of how to get that level of security
> in a language? Thanks.

a good example I think is
Jonathan Rees Security Kernel for the lambda calculus
http://mumble.net/~jar/pubs/secureos/

I noticed he recently posted a repository for it on github here
https://github.com/jar398/w7

I guess my question was can we get this without mucking about with
first class environments?
instead using the type system and I think it boils down to sort of,
if you add the set of free/non-local variables as a part of a
functions type, or (at least)
allow the language to discriminate between combinators (which have no
free/non-local variables)
and other functions with free variables.