9 ms·

Show HN: Peridot – A functional language based on two-level type theory

151 points by ehatti 4y ago

rowanG077 4y ago
From what I can tell this is having a term rewrite system integrated into your language. Is this significantly different then Haskell manual rewrites. Which I admit are sometimes brittle.
- fithisux 4y ago
  Not very knowledgeable but is there an equivalence between 2LTT and term rewriting?
  - ehatti 4y ago
    Not really. A detailed account of 2LTT can be found in this paper https://arxiv.org/abs/1705.03307 https://arxiv.org/abs/1705.03307 - 2LTT can be thought of as a general, type theoretic framework for metaprogramming.
    - simplify 4y ago
      Is there an introduction to 2LTT for those with only a basic understanding of type theory?
      - ehatti 4y ago
        Unfortunately there isn't, but I'll try my best here: In two level type theory, your language is actually two languages - a "meta language" (or meta level) and an "object language" (or object level). Additionally, we have a construct for relating object-level terms/types to meta-level terms/types. There are other, more type theory heavy qualifiers, but that's the basic idea. It's quite a simple system, but it turns out to subsume quite a lot of others. Depending on how your conversion construct behaves, you can get vastly different metaprogramming systems. The most important consideration when determining what you can do with 2LTT is how "similar" your two languages are, in a rough sense of the word. Remember that these really are two separate languages - they can have entirely different features and behave completely differently. Peridot is actually a good example, the object language is functional and dependently typed, while the meta language is more akin to λProlog or Twelf (it's a logic language). If the two languages are identical, you can get something akin to partial evaluation for example. Peridot is on the other end of the spectrum, where the languages are completely dissimilar. Note that 2LTT is actually even more broad than this. I'm talking specifically about 2LTT's applications to metaprogramming, but the authors of that paper used it to overcome some limitations of theorem proving in homotopy type theory. TL;DR: In two-level type theory, your language is really two languages (levels) stuck together. You also have a construct to relate object-level terms/types to meta-level terms/types (notably, the reverse is not allowed). Depending on how this construct works, you can get all kinds of metaprogramming systems.
- kthielen 4y ago
  You're right about term rewriting as a staged evaluation scheme. Similar to Haskell, I made this PL/compiler for Morgan Stanley where qualified type constraints (for e.g. type classes) are interpreted as stage-0 programs and rewritten into stage-1 programs that compile down to stage-2 programs (so a similar kind of stratification): https://github.com/morganstanley/hobbes https://github.com/morganstanley/hobbes It looks like this method is aimed at doing user pattern-matching on expressions in the first stage, kind of integrating Haskell-style rewrite rules in the main user language (rather than bolting them on the side in comments).
  - seertaak 4y ago
    Major language crush... Everything from the type system to the compilation model to c++ compat just oozes good taste. Glorious structural record types, real union types (my running theory is that expression-based languages lacking these - looking at you, rust - are insufferable) AND variants. Pattern matching, slices, unboxed arrays/primitives, eager evaluation... Damn I love it. Hobbes looks so totally frickin' awesome, I'm so going to play with this tonight. Incredible work! What would be really cool for this language is to hook into jupyterlab via xeus. It's not even that hard to do - I did it for my own (far inferior) toy language.
- ehatti 4y ago
  The difference is that it’s much more general - the metalanguage is an actual logic language, not limited to simple rewrites. You can (read: will be able to, haha) prove properties about meta-level program transformations. For those interested, I’m basing my system off of Twelf and Abella.
  - tluyben2 4y ago
    Any inspiration taken from Shen?
    - ehatti 4y ago
      I saw it a while back and thought the ideas were cool, but I didn’t check it out in enough detail to draw inspiration from it.
lisper 4y ago
Common Lisp has had this for decades: DEFINE-COMPIILER-MACRO.
- GolDDranks 4y ago
  But I have an impression that Common Lisp doesn't have a type system, whereas this languages strives to have all "levels" of it's metaprogramming typed, so it's not like this language doesn't have any novelty.
  - lisper 4y ago
    Common Lisp has a very sophisticated type system. The only thing it doesn't have (among things that are currently fashionable) is compile-time typing by default. Peridot is "novel" in that it introduces user-level compiler optimizations into a language that does have compile-time typing by default. But that's kind of like Chevrolet making a plug-in hybrid version of the C8 Corvette (which they recently announced they are going to do). Neither the C8 nor plug-in hybrids are new. A plug-in hybrid C8 will be new, and when it happens it will be a Big Deal to a niche market: the intersection of C8 fans and plug-in-hybrid fans. But it won't change the world. (For the record, I happen to be a member of the niche market to which a plug-in hybrid C8 will appeal, so I am very excited about it. So I get that some people may be excited about Peridot. I just think it's important to keep things in perspective.)
  - Mikeb85 4y ago
    Having dynamic typing != no type system.
    - lapinot 4y ago
      Actually no, not in programming language theory. What researchers call 'type system' is much more precise than what programmers call 'type system'. In the PL field, the behavior of a term is traditionally split into static behavior (described by types) and dynamic behavior (described by reduction/evaluation). What programmers call 'dynamic type systems' is just a way to instrument the runtime with dynamic data-shape checks. Note that most dynamic languages do have a non-trivial type system, where functions are typed with their number of arguments (eg static scoping and other structure-related static checks). Languages like bash otoh do really have a trivial type system, whith every term merrily going into the evaluator without any static/typing well-formedness analyzis. You might also be interested in gradual typing, which is about deriving systematic dynamic checks from a type system and then augmenting a given type system with an 'any' type to go into untyped (ie dynamically checked) mode.
bobbylarrybobby 4y ago
Reminds me of this paper on implementing compiler optimizations within the Julia language itself: https://arxiv.org/abs/2112.14714 https://arxiv.org/abs/2112.14714 -- "can symbolic mathematics do high-level compiler optimizations or vice-versa?"
lalaithion 4y ago
Is it possible to write an optimizer for something like `sum (filter is_even (range 0 100))` into a for loop, as to avoid materializing 2 lists in memory?
- sitkack 4y ago
  Doesn't inlining handle that case directly?
- ehatti 4y ago
  Yes. As I’ve said elsewhere, the system is not limited to simple term rewrites.
  - lalaithion 4y ago
    Is there an example of such a program? I don't see anything like that in the github repo.
    - ehatti 4y ago
      Unfortunately not! Embarrassingly, I haven't implemented pattern matching yet, which means functions like `sum` and `filter` can't be written. So far all my effort has gone towards the metaprogramming system. Bugfixing has me occupied at the moment, but after that I plan on doing pattern matching.
- tonyg 4y ago
  You might enjoy this paper, which presents "stream fusion", a technique which can do what you're talking about as well as a bunch of other cool stuff: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7401 http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7... "Stream Fusion: From Lists to Streams to Nothing at All." Duncan Coutts, Roman Leshchinskiy, Don Stewart. ICFP 2007.
  - cryptonector 4y ago
    Yes. I knew this as list fusion. Note that Rust doesn't need to do this because of the way `iter_into()` and mapping works. List fusion boils down to removing interior `.collect().iter_into()`. There is something to be said for designing APIs so that you don't need such rewrite rules, though, of course, the need comes up eventually anyways, so rewrite rules end up being kinda necessary.
lykahb 4y ago
Haskell has a RULES pragma that lets a user declare rewrites for the high-level optimizations that a compiler cannot deduce. They are most commonly used in the libraries. They are automatically applied by the compiler in the order of matching the AST from bottom-up. ``` {-# RULES "map/map" forall f g xs. map f (map g xs) = map (f.g) xs "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys #-} ``` Depending on the order of rules application, the quality of optimization can differ a lot. This fragility makes it harder to understand the impact of even a minor code change on the performance. It is also very hard to test that a particular optimization is applied, and to track down why if it's not.
- ehatti 4y ago
  Because of the nondeterminism we get from the metalanguage being a logic language, we don't have to worry about applying optimizers in a particular order. You can compose optimizers together, produce the possible results, and then select the best using a heuristic. Of course, the search space is potentially huge, so I'm looking into integrating constraints.

151 points by ehatti 4y ago

From what I can tell this is having a term rewrite system integrated into your language. Is this significantly different then Haskell manual rewrites. Which I admit are sometimes brittle.

fithisux 4y ago
Not very knowledgeable but is there an equivalence between 2LTT and term rewriting?
- ehatti 4y ago
  Not really. A detailed account of 2LTT can be found in this paper https://arxiv.org/abs/1705.03307 https://arxiv.org/abs/1705.03307 - 2LTT can be thought of as a general, type theoretic framework for metaprogramming.
  - simplify 4y ago
    Is there an introduction to 2LTT for those with only a basic understanding of type theory?
    - ehatti 4y ago
      Unfortunately there isn't, but I'll try my best here: In two level type theory, your language is actually two languages - a "meta language" (or meta level) and an "object language" (or object level). Additionally, we have a construct for relating object-level terms/types to meta-level terms/types. There are other, more type theory heavy qualifiers, but that's the basic idea. It's quite a simple system, but it turns out to subsume quite a lot of others. Depending on how your conversion construct behaves, you can get vastly different metaprogramming systems. The most important consideration when determining what you can do with 2LTT is how "similar" your two languages are, in a rough sense of the word. Remember that these really are two separate languages - they can have entirely different features and behave completely differently. Peridot is actually a good example, the object language is functional and dependently typed, while the meta language is more akin to λProlog or Twelf (it's a logic language). If the two languages are identical, you can get something akin to partial evaluation for example. Peridot is on the other end of the spectrum, where the languages are completely dissimilar. Note that 2LTT is actually even more broad than this. I'm talking specifically about 2LTT's applications to metaprogramming, but the authors of that paper used it to overcome some limitations of theorem proving in homotopy type theory. TL;DR: In two-level type theory, your language is really two languages (levels) stuck together. You also have a construct to relate object-level terms/types to meta-level terms/types (notably, the reverse is not allowed). Depending on how this construct works, you can get all kinds of metaprogramming systems.
kthielen 4y ago
You're right about term rewriting as a staged evaluation scheme. Similar to Haskell, I made this PL/compiler for Morgan Stanley where qualified type constraints (for e.g. type classes) are interpreted as stage-0 programs and rewritten into stage-1 programs that compile down to stage-2 programs (so a similar kind of stratification): https://github.com/morganstanley/hobbes https://github.com/morganstanley/hobbes It looks like this method is aimed at doing user pattern-matching on expressions in the first stage, kind of integrating Haskell-style rewrite rules in the main user language (rather than bolting them on the side in comments).
- seertaak 4y ago
  Major language crush... Everything from the type system to the compilation model to c++ compat just oozes good taste. Glorious structural record types, real union types (my running theory is that expression-based languages lacking these - looking at you, rust - are insufferable) AND variants. Pattern matching, slices, unboxed arrays/primitives, eager evaluation... Damn I love it. Hobbes looks so totally frickin' awesome, I'm so going to play with this tonight. Incredible work! What would be really cool for this language is to hook into jupyterlab via xeus. It's not even that hard to do - I did it for my own (far inferior) toy language.
ehatti 4y ago
The difference is that it’s much more general - the metalanguage is an actual logic language, not limited to simple rewrites. You can (read: will be able to, haha) prove properties about meta-level program transformations. For those interested, I’m basing my system off of Twelf and Abella.
- tluyben2 4y ago
  Any inspiration taken from Shen?
  - ehatti 4y ago
    I saw it a while back and thought the ideas were cool, but I didn’t check it out in enough detail to draw inspiration from it.

lisper 4y ago

Common Lisp has had this for decades: DEFINE-COMPIILER-MACRO.

GolDDranks 4y ago
But I have an impression that Common Lisp doesn't have a type system, whereas this languages strives to have all "levels" of it's metaprogramming typed, so it's not like this language doesn't have any novelty.
- lisper 4y ago
  Common Lisp has a very sophisticated type system. The only thing it doesn't have (among things that are currently fashionable) is compile-time typing by default. Peridot is "novel" in that it introduces user-level compiler optimizations into a language that does have compile-time typing by default. But that's kind of like Chevrolet making a plug-in hybrid version of the C8 Corvette (which they recently announced they are going to do). Neither the C8 nor plug-in hybrids are new. A plug-in hybrid C8 will be new, and when it happens it will be a Big Deal to a niche market: the intersection of C8 fans and plug-in-hybrid fans. But it won't change the world. (For the record, I happen to be a member of the niche market to which a plug-in hybrid C8 will appeal, so I am very excited about it. So I get that some people may be excited about Peridot. I just think it's important to keep things in perspective.)
- Mikeb85 4y ago
  Having dynamic typing != no type system.
  - lapinot 4y ago
    Actually no, not in programming language theory. What researchers call 'type system' is much more precise than what programmers call 'type system'. In the PL field, the behavior of a term is traditionally split into static behavior (described by types) and dynamic behavior (described by reduction/evaluation). What programmers call 'dynamic type systems' is just a way to instrument the runtime with dynamic data-shape checks. Note that most dynamic languages do have a non-trivial type system, where functions are typed with their number of arguments (eg static scoping and other structure-related static checks). Languages like bash otoh do really have a trivial type system, whith every term merrily going into the evaluator without any static/typing well-formedness analyzis. You might also be interested in gradual typing, which is about deriving systematic dynamic checks from a type system and then augmenting a given type system with an 'any' type to go into untyped (ie dynamically checked) mode.

bobbylarrybobby 4y ago

Reminds me of this paper on implementing compiler optimizations within the Julia language itself: https://arxiv.org/abs/2112.14714 https://arxiv.org/abs/2112.14714 -- "can symbolic mathematics do high-level compiler optimizations or vice-versa?"

lalaithion 4y ago

Is it possible to write an optimizer for something like `sum (filter is_even (range 0 100))` into a for loop, as to avoid materializing 2 lists in memory?

sitkack 4y ago
Doesn't inlining handle that case directly?
ehatti 4y ago
Yes. As I’ve said elsewhere, the system is not limited to simple term rewrites.
- lalaithion 4y ago
  Is there an example of such a program? I don't see anything like that in the github repo.
  - ehatti 4y ago
    Unfortunately not! Embarrassingly, I haven't implemented pattern matching yet, which means functions like `sum` and `filter` can't be written. So far all my effort has gone towards the metaprogramming system. Bugfixing has me occupied at the moment, but after that I plan on doing pattern matching.
tonyg 4y ago
You might enjoy this paper, which presents "stream fusion", a technique which can do what you're talking about as well as a bunch of other cool stuff: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7401 http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.7... "Stream Fusion: From Lists to Streams to Nothing at All." Duncan Coutts, Roman Leshchinskiy, Don Stewart. ICFP 2007.
- cryptonector 4y ago
  Yes. I knew this as list fusion. Note that Rust doesn't need to do this because of the way `iter_into()` and mapping works. List fusion boils down to removing interior `.collect().iter_into()`. There is something to be said for designing APIs so that you don't need such rewrite rules, though, of course, the need comes up eventually anyways, so rewrite rules end up being kinda necessary.

lykahb 4y ago

Haskell has a RULES pragma that lets a user declare rewrites for the high-level optimizations that a compiler cannot deduce. They are most commonly used in the libraries. They are automatically applied by the compiler in the order of matching the AST from bottom-up. ``` {-# RULES "map/map" forall f g xs. map f (map g xs) = map (f.g) xs "map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys #-} ``` Depending on the order of rules application, the quality of optimization can differ a lot. This fragility makes it harder to understand the impact of even a minor code change on the performance. It is also very hard to test that a particular optimization is applied, and to track down why if it's not.

ehatti 4y ago
Because of the nondeterminism we get from the metalanguage being a logic language, we don't have to worry about applying optimizers in a particular order. You can compose optimizers together, produce the possible results, and then select the best using a heuristic. Of course, the search space is potentially huge, so I'm looking into integrating constraints.