Recent searches
Search options
At the #agda headquaters:
"OK, guys, so our user pool consists only of folks who already know #haskell and #emacs Is there a way to narrow it down more?"
"I got it, what if we allow unicode, so they also have to also know #latex ?"
"Brilliant!"
(just kidding, agda is very cool (hope to learn it someday))
@abuseofnotation I REALLY want to learn it but Haskell is as advanced as I go at the moment.
@harryprayiv @abuseofnotation If you know Haskell, Agda is honestly not that bad. Yes, it’s more complicated, but much of the mindset is similar, as proofs are usually just ordinary recursive functions, using pattern matching to destruct the data structure.
for natural numbers, a recursive function corresponds exactly to classical induction proofs:
someProof : (n : Nat) -> SomeProperty n
someProof zero = baseCase
someProof (suc n) = inductionStep n (someProof n)
@LambdaDuck @harryprayiv Yeah, it's a pity that a language with such a simple core ended up so complex.
@LambdaDuck @abuseofnotation I’ve been dancing around type theory for a while now and it is *starting to* make sense by osmosis. So, maybe I will learn it. I’d like it to be useful, though and according to Simon Peyton Jones, it is probably even more useless than Haskell, which I already have a hard time convincing people I’m not just using for cool points from other geeks. ;)
@harryprayiv @LambdaDuck Can you give me context, I blocked youtube...
@abuseofnotation @LambdaDuck - https://redirect.invidious.io/watch?v=iSmkqocn0oQ
You can do this with most any YouTube video.