Hacker News Reader

Hacker News

Comment by ykonstant | Hacker News Reader

Full thread

ykonstant

I am dabbling in the cousin language Lean right now, and it is very fun to use!

View on HN

Some quick info for Lean:

Homepage: https://leanprover.github.io/

Source: https://github.com/leanprover/lean4

Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)

I also wrote a guide: https://agentultra.github.io/lean-4-hackers/

LEAN's syntax looks really great. I wish Scala could take some inspiration.

Scala's syntax is anyway quite similar already, but would need proper Unicode support and some other "tuning" like the `:=` and the `let monadic ← effect` syntax, imho.

One difference I see is Lean uses type classes while Idris uses implicits. Can anyone comment on the pros and cons of that decision? (Or pros and cons between the two languages in general?)

It also seems that Idris was created as a general-purpose language first, whereas Lean started as a proof assistant and only recently added general-purpose language. Is that evident when using the languages? A quick look at Lean's general-purpose language seems reasonably similar to the Indris experience AFAICT.

Imo the biggest difference is the "heritage", Lean is Coq inspired, Idris Agda inspired. This manifests in how people prove things. Idris has dependent pattern matching, so proofs are written as normal terms. Lean has tactics and proofs are small tactics scripts (which then generate the proof term behind the scene).

Other than that, the difference is mainly in infrastructure/libraries and community.

Well, idris (v2) is very special since it has modalities for compile-time erasure and linearity. This sets it apart from all the other dependently-typed languages. This makes it possible in theory (and currently being experimented with) to implement efficient-by-construction code.

https://arxiv.org/abs/2104.00480

Linearity is exclusive to Idris 2, compile time only values/run-time erasure are supported by all major proof assistants. Coq and Lean have the Prop type (compile time only) while Agda allows annotation of variables as run-time irrelevant.

And how does it compare to Arend? Does anybody know?

Are there any other HOT based languages out there? (Agda seems to have also some support for the "cubic version"; whatever this means, I'm actually clueless).

Cubical type theory is a way to get to a purely constructive foundation for Homotopy Type Theory. Super cool stuff from a foundations of math perspective and has some surprising applications to topological quantum computing but if it isn’t your rabbit hole you can probably not pay too much attention to it.

The whole "foundations of math" part is extremely exciting!

But I'm not an mathematician so I don't understand much (if anything). More in the programming languages "department" of interests.

But if something is "good enough" to describe whole math it could be useful for getting strong guaranties about programs, I guess. So I would be quite interested how this HOT stuff could be useful in practice. What could type systems based on this enable?

My limited understanding is that you get additionally "paths" between types and type constructor which denote equivalence between them.

But I have no clue what one could do with that (besides doing math, of course).

Speaking of cousin languages, it looks so much like Haskell.

Idris 1 was written in Haskell I think

Reply on news.ycombinator.com