Basically, I understand the concepts of functional programming quite well and can also programme #purescript or #haskell relatively confidently. But when it comes to #typelevel programming, I haven't quite got over this threshold yet. I would really like to understand everything better and learn more in this area, because many cool libraries are based on it.
@leobm It isn't purescript, but for an introduction to type level programming I will always recommend "TDD with Idris" by Dr. @edwinb . Idris and purescript syntax were both inspired by GHC Haskell, so the examples won't be too foreign, I hope.
That said, purescript is quite restricted when it comes to doing actual type-level programming. It doesn't have full dependent (Pi) types, and you have to do the existential = cps'd higher-rank universal just like in GHC. Do recent versions have GADTs?
@BoydStephenSmithJr@leobm@edwinb I think that in general, when it comes to type-level programming, it might be useful to look at a dependently-typed language (like Idris, but also Agda, Lean, ...) where this sort of stuff can more elegantly be done. Of course, Haskell currently has more libraries and more real-world applications, but many type-level concepts still feel bolted on, somewhat ugly, and you have to encode some things in weird ways because some stuff is simply missing. If you've seen these ideas how they're meant to be, then I think it's easier to understand them in Haskell or Purescript as well.
@kosmikus@leobm@edwinb Does Lean have passable stdin/stdout ? I know Agda has some, though I still haven't used it successfully -- Agda is mainly where I experiment with things to see if I can get them to type check.
I would like to see the many tutorials explain this using simple practical examples. I often find it difficult to understand the concepts in many tutorials on the subject because they are explained far too abstractly or you have to have prior knowledge, which I probably don't have after all.
@leobm The key point for me was understanding what “type A is inhabited by values x, y, z” is about.
Next, if types are some propositions in logic, then values are their proofs.
So, by writing code that compiles you’re proving that some logical statement holds.
Interestingly, if you can’t say something with types, no way you can write actual code that gonna work.
And of course, if a type system admits bullshit, then you can bullshit compiler with your code.
Every industrial language admits BS, but some of them make it easy to lie, cheat, AND steal (esp. with dynamic types), while the others make that painful.
A good type system can review your design before you have committed to implementing something unrealistic, being a net positive on effort spent pinning down all the important stuff.
Add comment