Idris2 - Tumblr Posts
Hey so, Type Families and Propositional Type Equality in Haskell are pretty cool even if I mostly used them as hacks for Haskell not having dependent typing.
First time I've heavily used Data.Type.Equality.
Rewriting proofs with `trans` is significantly more tedious in compound types and results in quite a few functions to help guide the types.
Overall pretty fun experience. Lack of `rewrite` really does ruin a lot of the satisfaction though.
(I also made it into a Kata)
Anyone else learn languages designed to be proof assistants? Or atleast designed with theorem proving as a usecase. Whilst barely knowing any pure Math?
When I first started learning Idris2, I had no idea how to even structure a proof. Needless to say I was quite lost, even if I was experienced in Haskell at that point.
Even now when I'm learning Lean, when I started which was about 5 days ago, I only knew how to prove with truth tables. It wasn't until yesterday when I found about the logics other than Classical.
So basically all I know about pure math is just me brute-forcing my way into learning languages like Idris as well as the occasional Haskell article or codewars kata ethat deep dives into a concept.
It wasn't until recently when I decided to finally sit down and learn Pure Math starting from basic Discrete Math. It's fun because I keep recognizing the concepts that's become commonplace in the languages I use. I learned about Connection intros and eliminations before knowing the difference between classical and intuitionistic logic.
What I'm saying is I love Curry-Howard correspondence