Pure: a modern functional programming language based on term rewriting | Hacker News Reader

Pure: a modern functional programming language based on term rewriting

agraef.github.io

128 pointsblacksqr34 comments

This is pretty neat! https://github.com/agraef/pure-lang/wiki/Rewriting#construct...:

> As a bonus, you also get "constructors with equations" for free. E.g., suppose that we want lists to automagically stay sorted and eliminate duplicates. In Pure we can do this by simply adding the following equations for the : constructor:

  > x:y:xs = y:x:xs if x>y; x:y:xs = x:xs if x==y;
  > [13,7,9,7,1]+[1,9,7,5];
  [1,5,7,9,13]

(The point about this global override is addressed later. The rewriting can be lexically scoped.)

Isn't this basically bubble sort?

No, the sources must be pre sorted for this to work. What this does is merge two lists of dynamic size like a set like a zipper.

I.e., Mergesort?

Eliminates duplicates too

If you build such a list by consing new elements to the front, then it's insertion sort. If you build the list from a balanced binary tree it's merge sort.

---

One important difference between this and quotient-inductive types is that there are examples of "types with equations" which cannot be expressed as a rewriting system, e.g., free groups.

It's a still a cool feature to have this built into the language.

> If you build the list from a balanced binary tree it's merge sort.

But in the example, the list is built by adding two lists. This means that in the example, it uses insertion sort which like bubble sort is O(n^2).

You're right and looking at the example again I was completely wrong (shouldn't post without coffee). You can implement merging by writing append (+) in the correct way. As written, the code will always insert a new element every time there is a cons (:).

One way of getting better performance "by default" is to construct lists with constructors for empty list, singletons and append and then adding equations to ensure that the resulting binary tree is balanced.

I don't think I've come across term-rewriting before. There's an example in their wiki page for inserting into a BST:

  > nonfix nil;
  > insert nil y         = bin y nil nil;
  > insert (bin x L R) y = bin x (insert L y) R if y<x;
  >                      = bin x L (insert R y) otherwise;
  > foldl insert nil [7,3,9,18];
  bin 7 (bin 3 nil nil) (bin 9 nil (bin 18 nil nil))

Lines beginning with > are what you type; the extra line is the evaluated response.

So the language is dynamically typed and it seems you don't need to declare constructor symbols that take arguments. A constructor seems to be something that is irreduceable according to the rules already defined, whereas a function is something with reduction rules available.

I'm not sure I agree with the rationale for the dynamic typing. The designer says it means the language supports an arbitrary degree of polymorphism, but obviously it means it accepts invalid programs with undefined behavior. I think by adopting a Typescript style system you'd get huge advantages ("Typescript-style" meaning structural, adhoc and evolving towards correctness, rather than meeting the wrong design constraints upfront). But I'm still not at all sure my intuitions for this language are useful.

Anyway that's my review in five minutes. I hope someone writes something relevant here.

> but obviously it means it accepts invalid programs with undefined behavior.

Congratulations! This is the most entitled sentence in all of computing. The prize ceremony will be held at your house, tomorrow. I'll be casting a statue of gold for you, but first I have to rebuild all the software between me and the CNC machine in Coq or Typescript.

On a barely related note: When did Typescript's type system become some shining example of type systems? It's super basic and you can do almost nothing with it. It's not as basic as Go's type system, but it's really very sparse.

Not saying it’s particularly amazing, but its ad-hoc structural product types are really nice. I would really enjoy if a language had TS-style ad-hoc structural products and Ocaml-style ad-hoc structural sums. This would allow for very lightweight type-level documentation.

I can no longer edit my original comment, so I'll take the opportunity to pull back a little bit and say I don't wanna make it seem like I think TS's type system is useless, but rather it's nothing special.

That said, I guess it's much better than nothing at all (JS).

>Ocaml-style ad-hoc structural sums

Ocaml also has ad-hoc products (objects and tuples).

Basically every language has ad-hoc products in the form of tuples. They aren’t structurally typed in ocaml, which is the interesting part. Typescript has labeled products that have similar subtyping rules to ocaml’s anonymous sum subtyping rules. Eg {x:a, y:b} < {x:a}.

Objects in OCaml are labeled products. < x:a; y:b > <: <x:a>

Ah, I did not know that. I’ve only used the {x : a} record syntax in ocaml.

What's up with Clean these days?

https://en.wikipedia.org/wiki/Clean_(programming_language)

I haven't heard mum about it since 2006. Wikipedia says the last stable release was in 2011. I guess the market for proprietary Miranda derivatives fell apart after _Real World Haskell_ was published?

I wish Clean caught on more. I find unique types a little easier to think about. A version of Clean could/can(?) compile Haskell too.

If I recall correctly, Clean is BSD licensed. By 'proprietary' do you mean their main source of funding was building proprietary solutions over what they release open source ? They did seem they were more of a 'windows first' group, but I may be wrong about that.

From what I've heard in the hallways, the people driving the language from the Radboud University retired.

Nothing it seems.

Too bad. Clean's graph rewriting and unique types approach was very good and practical direction for functional programming.

Declaring unique types allows functional paradigm in much lower lever programming and it's easy to grasp. (it's part of the linear types paradigm).

Is there an example of a problem where Pure would be a good choice of language in solving that problem?

From the FAQ:

Why Pure?

Thanks to LLVM, Pure offers state-of-the-art JIT compiler technology in an interactive environment, and makes it easy to interface to C in a direct fashion. Recent releases also provide the ability to directly import LLVM bitcode modules into Pure scripts and to inline code written in various languages (currently C/C++, Fortran and Faust). Scripts can also be compiled to standalone native executables (they are also executed during compilation, which makes it possible to employ partial evaluation techniques).

Pure has an efficient MATLAB-like, GSL-compatible matrix type which makes it easy to interface to languages and libraries for doing numeric computations and digital signal processing. In particular, Pure interfaces to (GNU) Fortran, Octave and Grame's Faust, and you can directly invoke GSL routines on Pure matrices. In a way, this is like having Haskell, Octave, DSP programming and the term rewriting capabilities of a computer algebra system under one hood.

It goes without saying that Pure can be used used for mathematical applications, but there's also a growing collection of extension modules for GUI, graphics, multimedia, database and web programming which makes Pure useful as a kind of algebraic/functional scripting language for a variety of purposes.

I don't think this really does a great job of selling Pure as a solution to a problem. It's sort of saying "Well, you can kind of use Pure for anything, even GUIs!".

I'm sure there's something Pure was designed to solve which could be brought forward as something it solves beautifully. It's not really obvious what that is from this text, though.

For me the symbolic math capabilities are interesting. I'm not sure I like the choice of reduce that much, but still few languages offer symbolic capabilities. Python does with SymPy and Maxima is based on Lisp but that's moe a case of a CAS being based on a language than the language having symbolic capabilities and then there is Mathematica (expense being the barrier).

Online, dynamic music synthesis. pure comes from pd I think, puredata, which has as default an unoptimized graphical language. pure can deal with real-world musical problems much better.

Compare to: Maude

https://en.wikipedia.org/wiki/Maude_system

Maude is a truly fascinating language. Its base computation model (no true operation order and pure term rewritting) is extremely innovative, and I've never seen another language like it.

While not a production ready language, I'm really surprised it or something like it doesn't get more attention.

Isn't just about any functional language based on term rewriting? E.g. beta reductions, combinators, etc.

Yes. The website beats around the bush before stating that actually most functional programming languages are just like this (possibly more interesting too, shh).

From 8 years ago:

https://news.ycombinator.com/item?id=722580

I wish it were modern enough to have a proper mobile site...

Reply on news.ycombinator.com