Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com