6 ms·
I am really enjoying lean 3 as a theorem prover; lean 4 as a programming language is a really intriguing/enticing prospect. The "functional but in place" paradi
by tomhoule 6y ago
I am really enjoying lean 3 as a theorem prover; lean 4 as a programming language is a really intriguing/enticing prospect. The "functional but in place" paradigm is something quite new, as far as I can tell. For reference, see the "Counting Immutable Beans" paper[1] by the designers of the language, that details how the runtime makes use of reference counts to do destructive updates in pure code whenever possible.
[1]: https://arxiv.org/pdf/1908.05647.pdf https://arxiv.org/pdf/1908.05647.pdf
- ivanbakel 6y agoA similar-but-different approach exists in (largely Dutch) research around uniqueness typing, which uses static analysis guarantees to allow for destructive updates wherever the compiler can prove something is uniquely referenced. To my knowledge, efforts have been made to integrate that approach into GHC.
- orbifold 6y agoI think the novel thing is that this is doing it dynamically, which bypasses the static analysis and makes it applicable to situations where static analysis wouldn't be useful.
- kmill 6y agoAs I understand it, it does some static analysis still. The big idea with the Perseus algorithm, I think, is that instead of lending a reference at a function call, it is given. This leads to numerous optimizations where memory can statically be reused. They still do dynamic checks that an object has only one reference, too, when it's not statically known.
- creata 6y agoAre you referring to Linear Haskell[0] or some other effort? Linear Haskell can definitely express destructive updates, but IIRC it needs unsightly stuff like constructors which take continuations and method signatures along the lines of length : Array a -o (Array a, Unrestricted Int) which have to thread the unique value through them, since there's no notion of borrowing. [0]: https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types
- ivanbakel 6y agoI'm talking about uniqueness typing. It's similar to linear types, but not the same. If you search the term, you can find a few research papers from Dutch universities, particularly around Clean, a programming languages which uses uniqueness typing instead of monads for IO.
- creata 6y agoThanks. I'm aware of that, but I can't find any such efforts for Haskell in particular.
- xiphias2 6y agoWhy is linear typing not implemented though? Can the theorem prover prove for some function that reference counting doesn't have to be used?
- tomhoule 6y agoI can't claim to know the details, but my understanding is that the interaction of linear typing with dependent types is an open research problem (see the quantitative type theory papers, for example). It's also a burden on the user rather than the runtime, so it's a tradeoff.
- xiphias2 6y agoIs it still a big burden if the theorem prover can automate checking that a function can be evaluated without ref counting / garbage collector? I understand that it's a very hard problem though.
- haskellandchill 6y agoI'm trying to understand why dependent types can't represent linearity since you can model Nat at type level in dependent types. Dependent types can do capability modeling at the type level and linearity (or affinity) seems like a capability. From this thread (https://www.reddit.com/r/haskell/comments/20k4ei/do_dependent_type_systems_subsume_linear_type/ https://www.reddit.com/r/haskell/comments/20k4ei/do_dependen...) it seems like it can be done. I'm looking for something more formal to explain the orthogonality (or simulatability) of linear types inside a dependent type system.
- chriswarbo 6y agoFrom my understanding, dependent types can model linearity, but you'd need to use that model type system rather than the 'native' type system (similar to how, for example, Bash can model OOP (e.g. using a mixture of naming conventions, associative arrays, eval, etc.), but isn't natively OOP). If we go down that route, we're essentially building our own programming language, which is inherently incompatible with the dependently-typed language we've used to create it (in particular: functions in the underlying language cannot be used in our linear-types language, since they have no linearity constraints). A common example is a file handle: I can prove that the 'close' function will produce a closed handle, e.g. close : Handle Open -> Handle Closed I can prove that those handles point to the same file: close : (f: Filename) -> Handle f Open -> Handle f Closed I can prove arbitrary relationships between the input values and the output value. Yet nothing I do restrict the structure of a term, like how many times a variable is used, to prevent e.g. foo h = snd (close h, readLine h) For that sort of control, we need to build the ability to track things into the term language itself; either by adding linear types (or equivalent) to the language, or building a new incompatible language on top (as I mentioned above).
- creata 6y agoLean has an array type, which the docs say is implemented much like a C++ vector or Rust Vec. But data types in functional programming languages all expose an immutable interface, so what happens when someone changes the list in two different ways? Is a new copy of the array made, is some variant of a persistent array used, or does the program just fail to compile? https://leanprover.github.io/lean4/doc/array.html https://leanprover.github.io/lean4/doc/array.html