5 ms·

> I tried to lookup "substructural types" but wasn't able to find anything. A substructural type system lets you express constraints on how many times a value

> I tried to lookup "substructural types" but wasn't able to find anything. A substructural type system lets you express constraints on how many times a value can be used. More precisely: (0) An object of an affine type cannot be used more than once. This is enforced by not allowing the same object to exist in multiple environments. Affinely typed objects can be moved (in the Rust sense) from one environment to another, but as soon as this happens, the object ceases to exist in the original environment. Affinely typed objects can be reclaimed as soon as they are first used (since they can't be used again) or go out of scope (since no other scope has access to them), so no dynamic garbage collection is necessary for them. (1) An object of a relevant type has to be used at least once. This is enforced by requiring the result of every computation to be fed into some other computation. In lazy languages, relevant types can be used for strictness optimizations: if the result of a computation is guaranteed to be used, then computing the result upfront eliminates the overhead of creating lazy suspensions. (2) An object of a linear type has to be used exactly once. A linear type is just a type that is both affine and relevant, so everything mentioned above applies. > How do things like closure/lambdas wok without GC? A closure has its own environment. With affine types, when a closure captures an object from the outer context, the object ceases to exist in the outer environment. This is how move closures already work in Rust. --- A digression: This is why I find GHC's plethora of type system extensions utterly disappointing. They marginally increase Haskell's expressiveness in areas where the language is already very expressive, but they don't address the language's limitations w.r.t. resource management. For instance, Haskell is incapable of statically enforcing that file handles won't leak.

tome 10y ago
> For instance, Haskell is incapable of statically enforcing that file handles won't leak. It is capable of it. You can do it with one monad transformer layer per file handle. Yes, that's utterly inconvenient, but you can do it. It would be far less inconvenient with (higher) row types.
- catnaroek 10y ago
  That forces you to deallocate resources in the inverse order of allocation, which may or may not be what you want. For example, the lock acquisition and release pattern used in the implementation of Lehman-Yao trees (and variants thereof) is inexpressible using monadic regions.
  - tome 10y ago
    Hmm, well I've never implemented this myself so I'm not going to contradict you, but I'd be really surprised if you can't hoist into the monad transformer stack and close off a lower region earlier than the top-level region.
    - catnaroek 10y ago
      Would this be safe if the destructor of an inner region requires objects from outer regions to still exist?
      - tome 10y ago
        I don't see how there could be any such requirements, if we're talking about file handles.
        catnaroek 10y ago
        I'm pretty sure DBMS implementors have to work with data structures whose nodes are spread across several files, and which have to be locked and unlocked in very precise ways to preserve the integrity of the data they contain. I'd like to be able these locking and unlocking patterns with types.
        deleted 10y ago
        [deleted]
cm3 10y ago
Mathieu Boespflug is from what I understand working on bringing linear types to ghc: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes https://ghc.haskell.org/trac/ghc/wiki/LinearTypes and https://redd.it/50nkbo https://redd.it/50nkbo
bogomipz 10y ago
Wow, thanks for the comprehensive answer. Its much appreciated.
ninesigns 10y ago
Re: last part Idris programming language has "Uniqueness types" [1], that are inspired by Clean and Rust. There is also an interesting talk [2] where Idris author discusses state/side-effects management. [1] http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html http://docs.idris-lang.org/en/latest/reference/uniqueness-ty... [2] https://www.youtube.com/watch?v=kpPyolN65s0 https://www.youtube.com/watch?v=kpPyolN65s0
- catnaroek 10y ago
  Statements like this one worry me a lot: > We also haven’t checked any of the metatheory, so this could all be fatally flawed! What I think makes the most sense is to have a nested hierarchy of type universes: (0) All types (1) Types that support sharing (data structures, first-class functions, but not ephemeral resources) (2) Types that support equality testing (data structures not containing first-class functions) Standard ML already has a similar hierarchy, but levels (0) and (1) are collapsed into a single one. At least it is intuitively obvious that this isn't wrong. The type safety proofs can come later. Also, I'd rather not have a notion of borrowing at all. It's fine for Rust, because it's a low-level language. But, in a high-level language, if you want to share data structures, just use garbage collection. And, if you really want to share mutable objects (which most of the time you shouldn't), use mutexes. Mutexes themselves don't exactly support sharing, but they can be explicitly cloned and locked.

tome 10y ago

> For instance, Haskell is incapable of statically enforcing that file handles won't leak. It is capable of it. You can do it with one monad transformer layer per file handle. Yes, that's utterly inconvenient, but you can do it. It would be far less inconvenient with (higher) row types.

catnaroek 10y ago
That forces you to deallocate resources in the inverse order of allocation, which may or may not be what you want. For example, the lock acquisition and release pattern used in the implementation of Lehman-Yao trees (and variants thereof) is inexpressible using monadic regions.
- tome 10y ago
  Hmm, well I've never implemented this myself so I'm not going to contradict you, but I'd be really surprised if you can't hoist into the monad transformer stack and close off a lower region earlier than the top-level region.
  - catnaroek 10y ago
    Would this be safe if the destructor of an inner region requires objects from outer regions to still exist?
    - tome 10y ago
      I don't see how there could be any such requirements, if we're talking about file handles.
      - catnaroek 10y ago
        I'm pretty sure DBMS implementors have to work with data structures whose nodes are spread across several files, and which have to be locked and unlocked in very precise ways to preserve the integrity of the data they contain. I'd like to be able these locking and unlocking patterns with types.
        deleted 10y ago
        [deleted]

cm3 10y ago

Mathieu Boespflug is from what I understand working on bringing linear types to ghc: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes https://ghc.haskell.org/trac/ghc/wiki/LinearTypes and https://redd.it/50nkbo https://redd.it/50nkbo

bogomipz 10y ago

Wow, thanks for the comprehensive answer. Its much appreciated.

ninesigns 10y ago

Re: last part Idris programming language has "Uniqueness types" [1], that are inspired by Clean and Rust. There is also an interesting talk [2] where Idris author discusses state/side-effects management. [1] http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html http://docs.idris-lang.org/en/latest/reference/uniqueness-ty... [2] https://www.youtube.com/watch?v=kpPyolN65s0 https://www.youtube.com/watch?v=kpPyolN65s0

catnaroek 10y ago
Statements like this one worry me a lot: > We also haven’t checked any of the metatheory, so this could all be fatally flawed! What I think makes the most sense is to have a nested hierarchy of type universes: (0) All types (1) Types that support sharing (data structures, first-class functions, but not ephemeral resources) (2) Types that support equality testing (data structures not containing first-class functions) Standard ML already has a similar hierarchy, but levels (0) and (1) are collapsed into a single one. At least it is intuitively obvious that this isn't wrong. The type safety proofs can come later. Also, I'd rather not have a notion of borrowing at all. It's fine for Rust, because it's a low-level language. But, in a high-level language, if you want to share data structures, just use garbage collection. And, if you really want to share mutable objects (which most of the time you shouldn't), use mutexes. Mutexes themselves don't exactly support sharing, but they can be explicitly cloned and locked.