Hacker News Reader

Comment by agumonkey | Hacker News Reader

After walking in the land of functions for a long time I wonder if there are advanced advanced languages.

Well, there's:

- Dependently typed languages (ATS, Agda, Idris)¹ should be fairly familiar if you're a Haskell veteran.

- Array languages (APL, J, K, and more obscure ones like Nial) are pretty enlightening if you're a functional programmer (at least they are for me). Most of these trace to Ken Iverson and his Notation as a Tool of Thought. They are a bit brain-bending at first, largely because of the density, but they're fun to use and the density makes comprehension easier after a while.

- Function-level languages (FL, FPr, J) – a somewhat obscure and very advanced sister to functional programming. If you're familiar with Haskell Arrows, there are many parallels. They are, essentially, a more convenient point-free style. Most (all?) of these trace to John Backus (of Fortran and Backus-Naur Form fame) and his 1977 Turing Award lecture Can Programming Be Liberated From the von Neumann Style?

J (http://jsoftware.com/) combines array and function-level programming, and IMO is a very good language to learn to expand your horizons if you're a veteran functional programmer.

¹ Coq kinda, but it's more of a theorem prover than a programming language. Agda sort of fits that too.

I had gnu apl installed (along with emacs mode:). APL and it's siblings are amazing, tiny, expressive, light.. lot to love. Juts nothing as mind bending as; say lambda calculus.

Didn't know FL/FPr were arrow-like. Didn't even know they were implemented .. I thought Backus quit because of IO.

Lots of people are suggesting the Idris/Agda road .. I guess I have my answer.

As far as FL/FP/FPr go, http://www.call-with-current-continuation.org/fp/ is the most mature and complete implementation I'm aware of.

There's #proglangdesign on freenode where a bunch of us have been on an array language/function-level streak lately. Some people there might be aware of more.

brilliant , I didn't know about the ccc impl nor the IRC chan. I know some folks that might be interested.

There's theorem provers like Coq. I'm pretty comfortable with Haskell, but concepts like the difference between Propositions and Booleans are enlightening to my Haskell the same way Haskell can be enlightening to use of other languages.

Cool, that's the kind of derivative I was looking for.

Have you explored languages with dependent type systems such as Agda, Idris, Coq, or Twelf?

You could also explore languages from an academic perspective. Benjamin Pierce has written several high quality texts about topics in programming languages.

Not yet (watching some youtube talks and introductory classes in college not couting). But even then I'm not sure they're more 'advanced' than Haskell. Do they implement the full lambda cube ? Even then it feels like constructive proofs are a 'normal' step after recursive functions. I'm curious about complete new way of thinking and modeling, something that would allow full graph exploration and multistaged/layered partial evaluation easily... from abstract concept down to signals and fixed-sized electronic compositions. I don't know what precisely. I don't want to say Categories because it's overloaded these days and I only know it through the 'monad tutorial' end, but I liked the idea of adjoint functors to jump back and forth between concepts.

ps: Esterel/Lustre synchronous programming comes to mind too, or Petri nets ..

You might enjoy attending programming language events such as OPLSS (all of the old lectures are online and free to watch) or ICFP. You get to learn about lots of new research in programming languages, and often, you'll have an opportunity to explore programming languages from different perspectives, including logic and category theory.

Agreed with siblings: Agda, Idris and the like are one option.

You can try Curry or Mercury for Logic/Functional cross.

Shen for something with Turing-complete type-system (by design, as opposed to C++ templates).

Do you know any array language? Like J or K (or APL, though personally I never dared). I can recommend J as a better documented and easier to get into language.

Have you seen Avail (http://availlang.org)? It looks very funny at first, but it is incredibly expressive.

What about Factor and Cat/Kitten? Stack-based languages, the latter additionally statically typed.

The language itself is not, but I would argue that the Wolfram Language has an advanced, advanced standard library.

I'm warry of Wolfram Lang. I'd need to see field report because I think what was demoed, as nice as it looks; is only the working subset. I feel a huge ontological mess underneath.

Reply on news.ycombinator.com