6 ms·

Hey, author here. I definitely didn't expect to see Tao on Hacker News. As is probably obvious, the language is extremely early in its life, and it's not practi

Hey, author here. I definitely didn't expect to see Tao on Hacker News. As is probably obvious, the language is extremely early in its life, and it's not practical to write anything but trivial examples in it yet. Please don't judge!

roguas 4y ago
Designing a PL is a hard complicated process, very slim portion of professional programmers are able to deliver some novelty here. I think any judgement should be treated as merely a feedback on the usefulness of this language. The effort alone is exceptional accomplishment. Take care.
- zesterer 4y ago
  Thanks for your kind words :)
dmix 4y ago
Nice work on the README. Gets right to the point about what it look likes and what the goals are.
code_biologist 4y ago
I remember a golden age of programming reddit and HN in the late 2000s that inspired me learn a bunch of new programming languages, Haskell the biggest influence among them. It seemed like people were always posting their own personal languages, lisps (I remember the hot takes on Arc lol), and such all the time. I have very fond memories of going through Jack Crenshaw's "Let's Build a Compiler" after seeing it posted a bunch of times, then trying to build my own language in a similar vein. Cheers to you, and I hope you're learning and having fun working on your project!
- zesterer 4y ago
  Thanks!
  - jrumbut 4y ago
    I too remember that time and it left me terribly jaded about the utility of new languages. This is the first I've seen in a while where I think the offering hits a spot on the tradeoff continuum that is distinctive and where I can picture many circumstances where I would want to use this language (the soundness aspect is a big part of that).
dataangel 4y ago
> A rather dogged and obnoxious opinion of mine is that the 'optimisation ceiling' for statically-typed, total functional programming languages is significantly higher than traditional imperative languages with comparably weak type systems. Curious about plans for this. When Haskell use exploded I followed a lot of the blogs talking about it someday being faster than C because purity made compiler reasoning easier and stream fusion and other things were going to change the world, but as time went on idiomatic Haskell never came even close to C. Now having a lot of performance experience I think a major factor is that functional languages insist on using lists for everything, which map poorly to hardware. Looking at your screenshots, it looks like it still employs the list paradigm.
- zesterer 4y ago
  So... I want to preface this by saying that I'm very, very far from being an expert on this topic. Although Tao's compiler has a MIR optimiser, it only covers the basics (inlining, constant folding + symbolic execution, etc.). I think one of the main reasons that Haskell failed to solve this is actually the same reason that many lower level languages failed: it places too many requirements on data representation. In the case of C/C++ and even (to a lesser extent) modern languages like Rust and Swift, this is because they make promises about representation to the programmer that allow you to circumvent aspects of the language and still write correct code: be it transmutation, casting, field offsets, etc. In the case of Haskell, lists have an entirely arbitrary length and the language makes no effort to constrain this requirement in the type system, meaning that the compiler can only speculatively optimise a list into an unboxed array. In a language with dependent types, it should be possible to constrain the size of a list with the type system, allowing the optimiser to do its job without need for speculative whole-program analysis. The other reason Haskell doesn't quite succeed is monomorphisation (or lack thereof). Haskell's support for first-class higher-ranked types means that the language can't feasibly make promises about monomorphisation, and as a result it needs to revert to boxing and dynamic dispatch far more than it really should. Conversely, Tao is designed to monomorphise in all cases from the start. Rust demonstrates that functional programming (and in particular, programming with higher-order functions) is more than possible to optimise very well, and it does this by promising monomorphisation through the type system, allowing the compiler to aggressively perform static dispatch and inlining. From what I've seen, GHC also fails to pick a lot of low-hanging fruit. The last time I checked (perhaps this has since changed) GHC often struggles with things like TCO and inlining in relatively simple cases as a byproduct of its design (all functions are dynamically dispatched by default, with inlining being a speculative optimisation). I need to do a little more writing about exactly what ideas I have for Tao, but other languages of similar ilk demonstrate that Haskell is very far from the pinnacle of what is possible (for example, Koka's Perceus reference reuse: https://koka-lang.github.io/koka/doc/book.html#why-perceus https://koka-lang.github.io/koka/doc/book.html#why-perceus).
agumonkey 4y ago
good luck
slavapestov 4y ago
I'm curious how you implement associated types and equivalences between them. In the most general case, this allows encoding an arbitrary finitely-presented monoid in the type system, and the word problem on finitely-presented monoids is undecidable. However, you mention your type checker is Turing-complete.
- zesterer 4y ago
  Yep, this is the case: the type-checker allows arbitrary computation to occur at compilation time. You can see some of that here, where I've implemented peano arithmetic/addition/multiplication/branching using the type system: https://github.com/zesterer/tao/blob/master/examples/type-astronomy.tao https://github.com/zesterer/tao/blob/master/examples/type-as... . I've not yet had the time or mental fortitude to implement something more non-trivial like N-queens or a Brainfuck interpreter, but perhaps eventually!
yccs27 4y ago
Tao looks super cool, and similar to the kind of language I'd personally make if I decided to create one. Kudos for actually implementing yours! Some specific questions about the language design: - Does your flavor of algebraic effects allow distinct effects of the same type (e.g. two separate int-valued `State`s)? I haven't seen anyone talk about this, but it seems like a potential problem with effects. - Do you have plans for making pattern matching extensible? I've thought a lot about how this could be possible with optics (the FP construction), but haven't found a nice solution yet.
- zesterer 4y ago
  > Does your flavor of algebraic effects allow distinct effects of the same type Could you give an example of what you mean by this? Multiple effects can be combined together (although I'm still working on handlers for multiple effects), for example: effect console = input + print fn greet_user : console ~ () = { print("Please enter your name:")!; let name = input!; print("Hello, " ++ name)!; } > Do you have plans for making pattern matching extensible? I have no plans as of yet. Extensible pattern-matching seems to me to be quite hard to unify with exhaustivity. Tao supports most of the patterns that Rust/Haskell supports.
  - throwaway17_17 4y ago
    I think GP is referring to having two effects, like State1 and State2, both of which allow for stateful effects on int references, and then being able to handle the effects uniquely for each effect. I think the underlying type theoretical question would be are Tao’s effects nominally vs. structurally typed. A more practical example would be having two state-like effects for use as different allocation/deallocation strategies.
    - zesterer 4y ago
      Tao's effects are nominally typed, so there's no way to accidentally mix them up in the way I assume you're describing. For example: # Define a new effect that yields to the caller effect yield A = A => () # A generator that emits numbers def one_two_three : yield Nat ~ () = { yield(1)!; yield(2)!; yield(3)!; } # Print the numbers to the console def main : io ~ () = { one_two_three handle yield Nat with n => print(n->show)! }
lisper 4y ago
Actually looks pretty interesting and impressive to me. One question: does numerical destructing require that one of the terms be a constant? What happens if I write y ~ a + b ? Also: > In Tao, arg:f is shorthand for f(arg) Did you mean arg -> f ?
- zesterer 4y ago
  > does numerical destructing require that one of the terms be a constant? Yes, the general pattern is `n + K`. I'm looking to expanding this to other operations in the future too. > Did you mean arg -> f ? Yes. I changed the syntax recently, but forgot to change the README. Thanks for pointing this out!
  - lisper 4y ago
    > Yes, the general pattern is `n + K`. OK, so what is the intended benefit of y ~ x + 1 over x = y - 1 ? I can see an obvious benefit if I can write y ~ x + z where neither x nor z is a constant and the resulting semantics invoke some kind of mathematical constraint management system or backtracking search a la Prolog, but if I'm constrained to write things that can be trivially transformed into a binding I don't see the point.
    - zesterer 4y ago
      I think my other answer here should provide an answer: https://news.ycombinator.com/item?id=31989227 https://news.ycombinator.com/item?id=31989227
      - lisper 4y ago
        Ah, that makes sense. Thanks!

roguas 4y ago

Designing a PL is a hard complicated process, very slim portion of professional programmers are able to deliver some novelty here. I think any judgement should be treated as merely a feedback on the usefulness of this language. The effort alone is exceptional accomplishment. Take care.

zesterer 4y ago
Thanks for your kind words :)

dmix 4y ago

Nice work on the README. Gets right to the point about what it look likes and what the goals are.

code_biologist 4y ago

I remember a golden age of programming reddit and HN in the late 2000s that inspired me learn a bunch of new programming languages, Haskell the biggest influence among them. It seemed like people were always posting their own personal languages, lisps (I remember the hot takes on Arc lol), and such all the time. I have very fond memories of going through Jack Crenshaw's "Let's Build a Compiler" after seeing it posted a bunch of times, then trying to build my own language in a similar vein. Cheers to you, and I hope you're learning and having fun working on your project!

zesterer 4y ago
Thanks!
- jrumbut 4y ago
  I too remember that time and it left me terribly jaded about the utility of new languages. This is the first I've seen in a while where I think the offering hits a spot on the tradeoff continuum that is distinctive and where I can picture many circumstances where I would want to use this language (the soundness aspect is a big part of that).

dataangel 4y ago

> A rather dogged and obnoxious opinion of mine is that the 'optimisation ceiling' for statically-typed, total functional programming languages is significantly higher than traditional imperative languages with comparably weak type systems. Curious about plans for this. When Haskell use exploded I followed a lot of the blogs talking about it someday being faster than C because purity made compiler reasoning easier and stream fusion and other things were going to change the world, but as time went on idiomatic Haskell never came even close to C. Now having a lot of performance experience I think a major factor is that functional languages insist on using lists for everything, which map poorly to hardware. Looking at your screenshots, it looks like it still employs the list paradigm.

zesterer 4y ago
So... I want to preface this by saying that I'm very, very far from being an expert on this topic. Although Tao's compiler has a MIR optimiser, it only covers the basics (inlining, constant folding + symbolic execution, etc.). I think one of the main reasons that Haskell failed to solve this is actually the same reason that many lower level languages failed: it places too many requirements on data representation. In the case of C/C++ and even (to a lesser extent) modern languages like Rust and Swift, this is because they make promises about representation to the programmer that allow you to circumvent aspects of the language and still write correct code: be it transmutation, casting, field offsets, etc. In the case of Haskell, lists have an entirely arbitrary length and the language makes no effort to constrain this requirement in the type system, meaning that the compiler can only speculatively optimise a list into an unboxed array. In a language with dependent types, it should be possible to constrain the size of a list with the type system, allowing the optimiser to do its job without need for speculative whole-program analysis. The other reason Haskell doesn't quite succeed is monomorphisation (or lack thereof). Haskell's support for first-class higher-ranked types means that the language can't feasibly make promises about monomorphisation, and as a result it needs to revert to boxing and dynamic dispatch far more than it really should. Conversely, Tao is designed to monomorphise in all cases from the start. Rust demonstrates that functional programming (and in particular, programming with higher-order functions) is more than possible to optimise very well, and it does this by promising monomorphisation through the type system, allowing the compiler to aggressively perform static dispatch and inlining. From what I've seen, GHC also fails to pick a lot of low-hanging fruit. The last time I checked (perhaps this has since changed) GHC often struggles with things like TCO and inlining in relatively simple cases as a byproduct of its design (all functions are dynamically dispatched by default, with inlining being a speculative optimisation). I need to do a little more writing about exactly what ideas I have for Tao, but other languages of similar ilk demonstrate that Haskell is very far from the pinnacle of what is possible (for example, Koka's Perceus reference reuse: https://koka-lang.github.io/koka/doc/book.html#why-perceus https://koka-lang.github.io/koka/doc/book.html#why-perceus).

agumonkey 4y ago

good luck

slavapestov 4y ago

I'm curious how you implement associated types and equivalences between them. In the most general case, this allows encoding an arbitrary finitely-presented monoid in the type system, and the word problem on finitely-presented monoids is undecidable. However, you mention your type checker is Turing-complete.

zesterer 4y ago
Yep, this is the case: the type-checker allows arbitrary computation to occur at compilation time. You can see some of that here, where I've implemented peano arithmetic/addition/multiplication/branching using the type system: https://github.com/zesterer/tao/blob/master/examples/type-astronomy.tao https://github.com/zesterer/tao/blob/master/examples/type-as... . I've not yet had the time or mental fortitude to implement something more non-trivial like N-queens or a Brainfuck interpreter, but perhaps eventually!

yccs27 4y ago

Tao looks super cool, and similar to the kind of language I'd personally make if I decided to create one. Kudos for actually implementing yours! Some specific questions about the language design: - Does your flavor of algebraic effects allow distinct effects of the same type (e.g. two separate int-valued `State`s)? I haven't seen anyone talk about this, but it seems like a potential problem with effects. - Do you have plans for making pattern matching extensible? I've thought a lot about how this could be possible with optics (the FP construction), but haven't found a nice solution yet.

zesterer 4y ago
> Does your flavor of algebraic effects allow distinct effects of the same type Could you give an example of what you mean by this? Multiple effects can be combined together (although I'm still working on handlers for multiple effects), for example: effect console = input + print fn greet_user : console ~ () = { print("Please enter your name:")!; let name = input!; print("Hello, " ++ name)!; } > Do you have plans for making pattern matching extensible? I have no plans as of yet. Extensible pattern-matching seems to me to be quite hard to unify with exhaustivity. Tao supports most of the patterns that Rust/Haskell supports.
- throwaway17_17 4y ago
  I think GP is referring to having two effects, like State1 and State2, both of which allow for stateful effects on int references, and then being able to handle the effects uniquely for each effect. I think the underlying type theoretical question would be are Tao’s effects nominally vs. structurally typed. A more practical example would be having two state-like effects for use as different allocation/deallocation strategies.
  - zesterer 4y ago
    Tao's effects are nominally typed, so there's no way to accidentally mix them up in the way I assume you're describing. For example: # Define a new effect that yields to the caller effect yield A = A => () # A generator that emits numbers def one_two_three : yield Nat ~ () = { yield(1)!; yield(2)!; yield(3)!; } # Print the numbers to the console def main : io ~ () = { one_two_three handle yield Nat with n => print(n->show)! }

lisper 4y ago

Actually looks pretty interesting and impressive to me. One question: does numerical destructing require that one of the terms be a constant? What happens if I write y ~ a + b ? Also: > In Tao, arg:f is shorthand for f(arg) Did you mean arg -> f ?

zesterer 4y ago
> does numerical destructing require that one of the terms be a constant? Yes, the general pattern is `n + K`. I'm looking to expanding this to other operations in the future too. > Did you mean arg -> f ? Yes. I changed the syntax recently, but forgot to change the README. Thanks for pointing this out!
- lisper 4y ago
  > Yes, the general pattern is `n + K`. OK, so what is the intended benefit of y ~ x + 1 over x = y - 1 ? I can see an obvious benefit if I can write y ~ x + z where neither x nor z is a constant and the resulting semantics invoke some kind of mathematical constraint management system or backtracking search a la Prolog, but if I'm constrained to write things that can be trivially transformed into a binding I don't see the point.
  - zesterer 4y ago
    I think my other answer here should provide an answer: https://news.ycombinator.com/item?id=31989227 https://news.ycombinator.com/item?id=31989227
    - lisper 4y ago
      Ah, that makes sense. Thanks!