3 ms·

the hopper language (the version used in this repo is an earlier snapshot of work from this fall that essentially a minimal scheme / lambda calculus with progra

the hopper language (the version used in this repo is an earlier snapshot of work from this fall that essentially a minimal scheme / lambda calculus with program level transactional memory) provides mechanisms for first class ownership. Current hopper master is under a huge amount of churn towards the full language we're building, so unless you enjoy reading compiler code bases under heavy active dev, the best i can say is this: stay tuned :) linear logic provides a nice vehicle for modelling first class ownership. namely: holding a value in a program IS owning it. That plus a lot of ideas from languages/tools like Agda, Coq, Lean, and Idris along with some of what i've learned being an occasional contributor to GHC, plus general PL tech, are going into Hopper, though the current code base

brighton36 11y ago
Will you be crowdfunding?
- carterschonwald 11y ago
  that not currently planned, thanks for asking! But once things are a little bit more mature (with the design a bit more visibly articulated, contributions / collaborations over at https://github.com/hopper-lang/hopper https://github.com/hopper-lang/hopper will be more than welcome :) I'm hoping to end up with a very nice tool that I hope will be used in a surprising diversity of situations, but such discussions will be more intelligible once its not just a compiler ir core and runtime :)
thedatabase 11y ago
Cool project! Are you using dependent linear types? Or are you using dependent types some places, and non-dependent linear types for the ownership semantics?
- carterschonwald 11y ago
  Excellent Question. The notion of linearity were starting with for type system design corresponds with runtime linear usage, which Means linear computations that are pure can be lifted into types because they don't have any runtime usage. One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like & Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake

brighton36 11y ago

Will you be crowdfunding?

carterschonwald 11y ago
that not currently planned, thanks for asking! But once things are a little bit more mature (with the design a bit more visibly articulated, contributions / collaborations over at https://github.com/hopper-lang/hopper https://github.com/hopper-lang/hopper will be more than welcome :) I'm hoping to end up with a very nice tool that I hope will be used in a surprising diversity of situations, but such discussions will be more intelligible once its not just a compiler ir core and runtime :)

thedatabase 11y ago

Cool project! Are you using dependent linear types? Or are you using dependent types some places, and non-dependent linear types for the ownership semantics?

carterschonwald 11y ago
Excellent Question. The notion of linearity were starting with for type system design corresponds with runtime linear usage, which Means linear computations that are pure can be lifted into types because they don't have any runtime usage. One of the More surprising / interesting realizations we had recently was that the copattern matching for coinductive Data as seen in Agda is exactly what's needed to define pattern matching sanely on certain linear type operators like & Which then let's you very succinctly model problems like having cake vs eating it. The original escrow of deliciousness vs the pretty cake