Pinned toot

Remember: TheAspiringHacker is no longer the username of my GitHub and GitLab accounts!

Pinned toot

As a corollary, if I ever toot anything political, please don't assume that the people whom I follow or who follow me agree with me.

Pinned toot

Disclaimer: In case it isn’t obvious, I do not necessarily share political beliefs with the people whom I follow or boost.

US Politics 

The type theory uprising 

The gamer uprising 

Shoot! I was planning to squash my commits, but forgot to when I merged + pushed!

Programming languages with tuple types are convenient because you don't have to define a new struct or class just to return some data from a function.

IMO this is similar to the benefit of anonymous functions, in which you don't need to define a named function just to pass a callback to something else.

Maybe we should call tuple types anonymous product types?

TAH boosted

@iitalics @jordyd so much agonism between MLs :blobsadleft: it's called ML family not ML enemey 😩

TAH boosted

I'm attempting to bolt my new Idris core onto the Blodwen front end. If you've ever implemented a dependently typed language, you'll know this is a sign of excellent progress!

TAH boosted

Only 8 source files away from bolting the Blodwen front end onto the new Yaffle core for Idris.

Yes, all these bits are named after 70s UK children's TV characters of varying levels of obscurity. I'm sure there are worse naming schemes.

The second reference in this article ( is a book by Saunders Mac Lane and another author, but the other author's name is replaced by a line. What does this mean?

Who coined the phrase "make illegal states unrepresentable?" Was it Yaron Minsky?

TAH boosted
TAH boosted

Metamorphosis by Kafka is about what happens to you and your family when you become a gamer


I would like to implement -style mixfix operators, but I don't understand the way that Agda resolves operators.

data T : Set where
t : T

_+_+_ : T -> T -> T -> T
t + t + t = t

_+_ : T -> T -> T
t + t = t

x : T
x = t + t + t

How does Agda decide which operator to use?

Shame on Jane Street for using the word "ML" this way! I had expected much better from this company!

I currently use Jane Street's Core_kernel (as opposed to Base) because I need doubly linked lists. However, Core_kernel is too bloated, so I am going to roll my own linked lists.

If I keep the API the same, will I have copyright issues? (Isn't this what the Oracle v Google case is about?)

Show more
Functional Café is an instance for people interested in functional programming and languages.