Effect system

[evincarofautumn]

It needs to be reinstated. Tentative core effects:

• IO = ST<GlobalHeap> + Fail
• ST<h :: Heap> = Read<h> + Write<h> + Alloc<h>
• Fail (computations that may cause task failure)

[evincarofautumn]

More thoughts:

• IO, Fail :: Effect
• ST, Read, Write, Alloc :: Heap -> Effect
• h1 * h2 = If heaps h1 and h2 are separate, then ST<h1> and ST<h2> are separate.

[strager]

Woah woah. IO shouldn't be related to memory. Just syscalls like write() and such.

[dmbarbour]

Maybe skip the name 'IO' (except maybe as a common aggregate) and just use 'Filesystem' vs. 'Network' vs. etc.

On Wed, Feb 19, 2014 at 10:51 PM, strager notifications@github.com wrote:

Woah woah. IO shouldn't be related to memory. Just syscalls like write() and such.

— Reply to this email directly or view it on GitHubhttps://github.com/evincarofautumn/kitten/issues/118#issuecomment-35589197 .

[evincarofautumn]

Okay, IO should refer to anything that interacts with the outside world—syscalls and foreign imports. The global heap is in the land of Kitten, so it doesn’t belong in IO. We can alias Global = ST<GlobalHeap>, make IO primitive for now, and break it down into Filesystem &c. in the future. Sound good?

[dmbarbour]

Just a thought: for foreign imports, consider an 'effect' for each library. Would improve portability and security.

On Thu, Feb 20, 2014 at 12:36 PM, Jon Purdy notifications@github.comwrote:

Okay, IO should refer to anything that interacts with the outside world—syscalls and foreign imports. The global heap is in the land of Kitten, so it doesn’t belong in IO. We can alias Global = ST, make IO primitive for now, and break it down into Filesystem &c. in the future. Sound good?

— Reply to this email directly or view it on GitHubhttps://github.com/evincarofautumn/kitten/issues/118#issuecomment-35653709 .

[evincarofautumn]

That would be cool, but probably not worth the effort. I don’t want any kind of foreign import declarations—I plan to simply parse included C headers, and they almost always lack a clear definition of “library”.

[evincarofautumn]

The new compiler has:

• IO—permission to break referential transparency
• Fail—permission to abort
• Unsafe—permission to break memory safety

Still need the ability to write permissions with type parameters, and declare type constants for heaps. Implementing that will also make it easier to add extensible records, as they would use similar type inference machinery.