Bluefin is a capability system

[Vinícius dos Santos Oliveira]

https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/

[William ML Leslie]

On Thu, 3 Sept 2026 at 07:56, Vinícius dos Santos Oliveira <vini.i...@gmail.com> wrote:

https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/

I'm doubtful that you can do a capability system in haskell, given the existence of unsafePerformIO.

I have had people try to tell me that Linux is a capability system, because it has file descriptors.  You can't get a capability system by adding strong references, one also has to remove authority that is not represented by capabilities.

--

William ML Leslie

Plausible, not normative.

[William ML Leslie]

On Thu, 3 Sept 2026 at 12:49, William ML Leslie <william.l...@gmail.com> wrote:

On Thu, 3 Sept 2026 at 07:56, Vinícius dos Santos Oliveira <vini.i...@gmail.com> wrote:

https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/

I'm doubtful that you can do a capability system in haskell, given the existence of unsafePerformIO.

I clicked through this reference, which is a really comprehensive post!

https://roscidus.com/blog/blog/2023/04/26/lambda-capabilities/

It mentions that this is called "safe haskell".  I was not aware of this.

[Matt Rice]

On Sat, Sep 5, 2026 at 5:43 AM William ML Leslie

<william.l...@gmail.com> wrote:
>
> On Thu, 3 Sept 2026 at 12:49, William ML Leslie <william.l...@gmail.com> wrote:
>>
>> On Thu, 3 Sept 2026 at 07:56, Vinícius dos Santos Oliveira <vini.i...@gmail.com> wrote:
>>>
>>> https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/
>>>
>>
>> I'm doubtful that you can do a capability system in haskell, given the existence of unsafePerformIO.
>
>
> I clicked through this reference, which is a really comprehensive post!
>
> https://roscidus.com/blog/blog/2023/04/26/lambda-capabilities/
>
> It mentions that this is called "safe haskell". I was not aware of this.
>

Cool, I'm curious if anyone knows of anything along these lines that
also has something that tracks memory allocations as effects too,
with something like keykos spacebanks. Koka seems to have an alloc
effect, but it doesn't quite seem to correlate to not producing the
alloc effect == no memory based denial of service. It seems like the
alloc effect is more about allocation of shared references, than space
usage.

Plus it allows "benign effects", which if you alloc/dealloc within the
function the effects cancel one another out.
But that seems like it is not so benign for the case where you try to
allocate more than available memory.
Where presumably there are two options, either panic or never return.

[William ML Leslie]

On Sun, 6 Sept 2026 at 06:55, Matt Rice <rat...@gmail.com> wrote:

Cool, I'm curious if anyone knows of anything along these lines that
also has something that tracks memory allocations as effects too,
with something like keykos spacebanks. Koka seems to have an alloc
effect, but it doesn't quite seem to correlate to not producing the
alloc effect == no memory based denial of service. It seems like the
alloc effect is more about allocation of shared references, than space
usage.

Plus it allows "benign effects", which if you alloc/dealloc within the
function the effects cancel one another out.
But that seems like it is not so benign for the case where you try to
allocate more than available memory.
Where presumably there are two options, either panic or never return.

Have you and I spoken about Tofte & Birkedal's "A Region Inference Algorithm", used in the MLKit compiler? (I feel like we have, but it was a few moons ago.)

Viewed from the right angle, a function's region type and effect in that scheme can identify:

- how much of the return value is freshly allocated, how much is constant, how much came from the parameters, and how much came from the lexical scope.

- any reads and writes to values found via the lexical scope or via arguments.

- any internal lexical capture, e.g. if a function is returned that retains access to an argument.

I remember thinking it would not be too challenging to extend that model to figure out which regions are statically bounded in size (and then trivially to determine whether a function uses a region unbound in size).  I don't know if anyone did that work.  I didn't figure out if/when there's a nice way to linearise all allocations and avoid all moves, assuming allocations are bounded for the duration of a function.

It would be very useful to safely bound a function's memory use, even if that might depend on the parameters given.  This problem has a really nice structure too, in that a function's memory use is the maximum of the memory use of each operation in the function.

[Matt Rice]

On Sun, Sep 6, 2026 at 6:25 AM William ML Leslie
<william.l...@gmail.com> wrote:
>
> On Sun, 6 Sept 2026 at 06:55, Matt Rice <rat...@gmail.com> wrote:
>>
>> Cool, I'm curious if anyone knows of anything along these lines that
>> also has something that tracks memory allocations as effects too,
>> with something like keykos spacebanks. Koka seems to have an alloc
>> effect, but it doesn't quite seem to correlate to not producing the
>> alloc effect == no memory based denial of service. It seems like the
>> alloc effect is more about allocation of shared references, than space
>> usage.
>>
>> Plus it allows "benign effects", which if you alloc/dealloc within the
>> function the effects cancel one another out.
>> But that seems like it is not so benign for the case where you try to
>> allocate more than available memory.
>> Where presumably there are two options, either panic or never return.
>
>
> Have you and I spoken about Tofte & Birkedal's "A Region Inference Algorithm", used in the MLKit compiler? (I feel like we have, but it was a few moons ago.)
>

Yeah, I believe at least it was discussed on the BitC lists which
would have been moons ago, and I did spend time reading their paper at
that time.
I probably wasn't thinking about it in these terms either as BitC
wasn't really aiming to be any kind of capability language,
and this seems to definitely be crossing more into that space.

> Viewed from the right angle, a function's region type and effect in that scheme can identify:
>
> - how much of the return value is freshly allocated, how much is constant, how much came from the parameters, and how much came from the lexical scope.
> - any reads and writes to values found via the lexical scope or via arguments.
> - any internal lexical capture, e.g. if a function is returned that retains access to an argument.
>
> I remember thinking it would not be too challenging to extend that model to figure out which regions are statically bounded in size (and then trivially to determine whether a function uses a region unbound in size). I don't know if anyone did that work. I didn't figure out if/when there's a nice way to linearise all allocations and avoid all moves, assuming allocations are bounded for the duration of a function.
>
> It would be very useful to safely bound a function's memory use, even if that might depend on the parameters given. This problem has a really nice structure too, in that a function's memory use is the maximum of the memory use of each operation in the function.
>

Indeed, I'm almost of a mind to start working on a "type safe manual
memory management programming language zoo", comparing region based,
to substructural, and separation logic based ones but I've got two
open projects I'm working on and one more on the shelf already.

[Pierre Thierry]

Le 03/09/2026 à 04:49, William ML Leslie a écrit :

On Thu, 3 Sept 2026 at 07:56, Vinícius dos Santos Oliveira <vini.i...@gmail.com> wrote:

https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/

I'm doubtful that you can do a capability system in haskell, given the existence of unsafePerformIO.

Safe Haskell lets you verify that no such escape hatch is used in the module you're compiling, nor any module imported, transitively.

With Safe Haskell, you remove globally mutable state, because by using unsafePerformIO, you can put a mutable reference in a variable exported by a module. With Safe Haskell, this isn't possible anymore. Any mutable state can only be used downstream of if its creation in a IO action.

Curiously,
Pierre Thierry
--

pie...@nothos.net
0xD9D50D8A

[Mark S. Miller]

On Sat, Sep 5, 2026 at 5:43 AM William ML Leslie <william.l...@gmail.com> wrote:

On Thu, 3 Sept 2026 at 12:49, William ML Leslie <william.l...@gmail.com> wrote:

On Thu, 3 Sept 2026 at 07:56, Vinícius dos Santos Oliveira <vini.i...@gmail.com> wrote:

https://h2.jaguarpaw.co.uk/posts/bluefin-capability-system/

I'm doubtful that you can do a capability system in haskell, given the existence of unsafePerformIO.

I clicked through this reference, which is a really comprehensive post!

https://roscidus.com/blog/blog/2023/04/26/lambda-capabilities/

It is indeed. I didn't know about this one. Thanks!

 

It mentions that this is called "safe haskell".  I was not aware of this.

--

William ML Leslie

Plausible, not normative.

--
You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/friam/CAHgd1hHivEPipMrjkJvBwx8YH8Dvgn-TUsbXyAVJPu7rkRzeKg%40mail.gmail.com.

--

  Cheers,
  --MarkM

[Rob Meijer]

Linux can come pretty close with MAC and FUSE.

It's old, but here is a Linux Journal article I wrote (with some great input from Jed) many years ago that goes into the subject:

https://www.linuxjournal.com/article/10199

--

You received this message because you are subscribed to the Google Groups "friam" group.
To unsubscribe from this group and stop receiving emails from it, send an email to friam+un...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/friam/CAHgd1hGYYqP%2B8i-_wHs7OXd3s964g8xA_P12Co%2BR3vymfc7wUA%40mail.gmail.com.