Re: cap patterns in 1ml

On Mon, Jan 25, 2016 at 1:17 PM, Matt Rice <[email protected]> wrote:

>
> 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.

I should have probably extrapolated on this,

foo 'a 'b (state:a) (constructor:a => b) = constructor(state)

so via 'a => b' a is pure, it can't smuggle anything out at
constructor call time.

foo 'a 'b (state:a) (constructor:a ={}> b) = constructor(state)

or some syntax where ={}> denotes pure combinator, it can't steal anything at
constructor time, and it contains no free variables that can be used to
smuggle anything at post-constructor foo(...).something(...) call time.

the main concern with this is 'state', any read-write references
provided in state
may have a reference to a reference stowed away, similarly any
function in 'state'
should be a combinator...

there is a chicken/egg problem though such that some oracle is
required to protect predecessors from successors or a trusted 3rd
party, or human scrutiny of the types as-per above,

hence the name 'foo' rather than 'factory'. I'm not sure exactly what
should be done about state (if anything)

but the general idea is that 'a and state (of type a) denote the
innards 'b' describes the types of parameters and return values that
can enter/escape, and constructor constructs some kind of a 'b' to
interact with using what it gets from state...
both parties in general agree to some terms about 'a and 'b.

anyhow...