Haskell - Tumblr Posts
ok i. love haskell
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
Yeah, though the general approach to not use it in larger projects due to performance faults. Generally Text is used which stores it internally as an array. Bytestring for byte info otherwise. Though a neat thing is most Haskell parser libraries can use any type by abstracting it via Stream. So something like parsec can directly work with String, Text, Bytestring, or even Tokenized lists. I recently used an indentation sensitive stream.
Going to see how someone else is doing a parser in haskell (using a library bc apparently haskell strings are lists of characters and not arrays? Interesting) I think seeing another functional programming approach might be better.
Stuff like these are what makes me both love and hate Haskell
Found you can define each fold via the other
as well as a mutually recursive definition, but only for the foldl_ side. I tried defining foldr_ via foldl_ but it was incorrect.
though for some reason, even if foldr_ is incorrect, foldl_ is still correct.
Anyways send me your most esoteric definitions of foldl and foldr
Stuff like these are what makes me both love and hate Haskell
I accidentally messed up the definition of foldl'''' it should be foldl'''' k z0 xs = let foldFunction = foldr (flip (.)) $ map (flip k) xs in foldFunction z0 Oh yeah an explanation: essentially, both fold functions can be viewed as:
foldr f z [x₀, x₁, x₂] = f x₀ (f x₁ (f x₂ z)) foldl f z [x₀, x₁, x₂] = f (f (f z x₀) x₁) x₂
The Haskell foldl is defined via foldr. It does it mainly by turning every element in xs into a function. this is most evident when you rewrite it as
foldl_ :: (b -> a -> b) -> b -> [a] -> b foldl_ f z0 xs = let accF = foldr (flip (.)) id $ map (flip f) xs in accF z0
And it becomes even more obvious in a β reduction some extra definitions (.) f g = \x -> f (g x)
flip f x y = f y x
-- Initial foldl f z [x₀, x₁, x₂] -- foldl definition let accF = foldr (flip (.)) id $ map (flip f) [x₀, x₁, x₂] in accF z -- map reduction let accF = foldr (flip (.)) id $ [flip f x₀, flip f x₁, flip f x₂] in accF z -- foldr reduction let accF = flip (.) (flip f x₀) (flip (.) (flip f x₁) (flip (.) (flip f x₂) id)) in accF z -- flip (.) reduction let accF = (.) ((.) ((.) id (flip f x₂)) (flip f x₁)) (flip f x₀) in accF z -- (.) reduction let accf = \x -> (\x -> (\x -> id ((flip f x₂) x)) ((flip f x₁) x)) ((flip f x₀) x) in accF z -- β reduction let accf = \x -> id ((flip f x₂) ((flip f x₁) ((flip f x₀) x))) in accF z -- flip reduction let accf = \x -> id (f (f (f x x₀) x₁) x₂ ) in accF z -- id reduction let accf = \x -> f (f (f x x₀) x₁) x₂ in accF z -- accf reduction f (f (f z x₀) x₁) x₂
and we end up with the original `foldl f z [x₀, x₁, x₂] = f (f (f z x₀) x₁) x₂` definition
Stuff like these are what makes me both love and hate Haskell
In Haskell there's the `(.).(.)` combinator called the boobies, which like most combinators, is named after a bird (Mockingbird, Cardinal, Bluebird, Kestrel, etc.)