Dependable Types 4: Terms Are Types Are Terms

Hello again! Sorry for the wait; it has been a very busy few months, but we’re back for the final part of the series: evaluation! Once we have our program written, how do we use it? How do we give it input and, from that, compute output? Today, we’re going to try perhaps a more unusual approach: converting our Expression to an actual Idris function. To do that, we’re going to need some real dependently-typed magic.

Dependable Types 3: Reductio Sine Absurdum

Welcome back! This time, we’re going to write that evaluate function we mentioned in the last article… Strictly, this function will be better named reduce, as it will perform an operation called beta reduction (or β-reduction, if you’re so inclined). What this means is that, any time we see an Abstraction on the left-hand side of an Application, we can simplify by taking the abstraction’s body, and replacing any mention of its parameter with the argument.

Dependable Types 2: Correctness by Construction

Part two already, is it? Well, I suppose it’s about time to write some code! Last time, we covered the constructions of the lambda calculus, as well as De Bruijn indices. Today, we’re going to cover basically the same thing, but encoding everything we learnt in Idris! If you’re not familiar with Idris or dependently-typed programming, things are going to start getting… weird.

Dependable Types 1: Full-STλC Development

Hello again! Been a while, right? Sorry for being AWOL the best part of six months; I got my dream job writing Haskell and PureScript with some brilliant minds over at Habito, and I’ve had a lot to learn! Anyway, one such mind is Liam, (who’ll be a familiar face to anyone getting stuck in with PureScript), and we have been spending our lunch times on various little projects. So, I thought it’d be cool to share one of these projects with you!

Fantas, Eel, and Specification 19: Semigroupoid and Category

It’s not goodbye, Fantasists. We’ll have other projects, new memories, more chance encounters. Let’s end on a high: talking about the humble Category, and how we’ve been learning this since the beginning. While it may not be the most immediately useful structure, it’s a gem for the curious.

Fantas, Eel, and Specification 18: Bifunctor and Profunctor

The worst is behind us. We’ve mastered the Monad, conquered the Comonad, and surmounted the Semigroup. Consider these last two posts to be a cool-down, because the end is in sight. Today, to enjoy our first week of rest, we’re going to revise functors. A number of times, we’ve seen types with two inner types: Either, Pair, Task, Function, and so on. However, in all cases, we’ve only been able to map over the right-hand side. Well, Fantasists, the reason has something to do with a concept called kinds that we won’t go into. Instead, let’s look at solutions.

Fantas, Eel, and Specification 17: Comonad

‘Ello ‘ello! Remember that Monad thing we used to be afraid of, and how it just boiled down to a way for us to sequence our ideas? How Extend was really just Chain backwards? Well, today, we’ll answer the question that I’m sure has plagued you all week: what is a backwards Monad?

Fantas, Eel, and Specification 16: Extend

You’re still here? That means you survived Monad! See? Told you it isn’t that scary. It’s nothing we haven’t already seen. Well, today, we’re going to revisit Chain with one slight difference. As we know, Chain takes an m a to an m b with some help from an a -> m b function. It sequences our ideas. However, what if I told you… we could go backwards? Let’s Extend your horizons.

Fantas, Eel, and Specification 15: Monad

Today is the day, Fantasists. We all knew it was coming, but we hoped it wouldn’t be so soon. Sure enough, though, here we are. We’ve battled through weeks of structures, and reached the dreaded Monad. Say your goodbyes to your loved ones, and let’s go.

Fantas, Eel, and Specification 14: ChainRec

Happy Tuesday, Fantasists! Sorry for the wait; I’ve been chasing around an issue to change this entry! No movement on that yet, so let’s soldier on! We’ve seen that chain allows us to sequence our actions, which means we can now do pretty much anything we want! As fellow JavaScripters, this is of course the time we get cynical; it can’t be that simple, right? Absolutely not, and let’s take a look at a convoluted example to show us why!

Fantas, Eel, and Specification 13: Chain

You told me to leave you alone. My Papa said, “Come on home”. My doctor said, “Take it easy”, but your lovin’ is much too strong. I’m added to your… Chain, Chain, Chain! Maybe we didn’t compose that one, but we’re going to compose plenty of things today!

Fantas, Eel, and Specification 12: Traversable

It’s Traversable Monday™, everyone! Granted, tomorrow would have made for a catchier opening, but I wasn’t thinking this far ahead when I picked the day to release these. Still, I bet you can’t wait for Monads now! Putting all that aside, does everyone remember how great the insideOut function from the Applicative post was? Well, today’s post is all about your new favourite typeclass.

Fantas, Eel, and Specification 11: Foldable

Welcome back, Fantasists! This week has been hectic, so I haven’t caught up the companion repository as I’d hoped to. However, I should have some time to devote to it this week, so watch this space! Anyway, why don’t we have some down time before we get onto the really grizzly parts of the spec? Let’s take a look at Foldable.

Pairs as Functors

Two-ish weeks ago, we talked about the wonderful flexibility of Function when you start treating it as a Functor. We started off with composition, then branching composition, and then finally environment-aware composition. We also gave our humble function a new name: Reader. Today, we’re going to walk the same path for Pair, and build up a closely-related idea.

Fantas, Eel, and Specification 9: Applicative

I asked my German friend whether any of this series’ posts particularly stood out. They said 9, so I’d better make this a good one! I told you we were doing jokes now, right? Moving on… Today, we’re going to finish up a topic we started last week and move from our Apply types to Applicative. If you understood the Apply post, this one is hopefully going to be pretty intuitive. Hooray!

Functions as Functors

Hello! I was explaining the other day how Function’s implementations of the different typeclasses can be useful, and I thought I might as well write them up in case they can be useful to someone. It’s also much easier than writing 140-character blocks. Specifically, we’ll go through Functor, Apply, and Chain, with examples all the way.

Fantas, Eel, and Specification 8: Apply

Aaand we’re back - hello, everyone! Today, we’re going to take another look at those mystical Functor types. We said a couple weeks ago that functors encapsulate a little world (context) with some sort of language extension. Well, what happens when worlds collide? Let’s talk about Apply.

Fantas, Eel, and Specification 3.5: Ord

Honestly, at this rate, the spec is going to grow faster than this blog series… We interrupt our usual schedule to introduce Fantasy Land’s newest member: let’s welcome Ord! Spoiler alert: if you’ve been following this series, this is going to be a pretty easy one.

Fantas, Eel, and Specification 7: Contravariant

Well, well, well. We’re a fair few weeks into this - I hope this is all still making sense! In the last article, we talked about functors, and how they’re really just containers to provide “language extensions” (or contexts). Well, today, we’re going to talk about another kind of functor that looks… ooky spooky:

Fantas, Eel, and Specification 6: Functor

Fantasy Landers, assemble! We’ve been concatenating for two weeks now; are you ready for something a bit different? Well, good news! If you’re humming, “Oh won’t you take me… to functor town?”, then this is the article for you. Today, friends, we’re going to talk about functors.

Fantas, Eel, and Specification 5: Monoid

Good Tuesday, Fantasists! This week, we’re going to take a quick(!) look at the semigroup’s older sibling: the monoid. We saw last week that a Semigroup type is one that has some concept of combining values (via concat). Well, a Monoid type is any Semigroup type that happens to have a special value - we’ll call it an identity value - stored on the type as a function called empty.

Fantas, Eel, and Specification 4: Semigroup

Today, after a moment of thanks to all those following this series (seriously, thank you ♥), we can move onto a question that has occupied human thought for aeons: how do we generalise the process of combining (or mooshmashing) things together? With semigroups, of course!

Fantas, Eel, and Specification 1: Daggy

Hello again, the Internet! As a functional programming zealot* and JavaScript developer, I spend a lot of my time raving about their crossover. In this series, we’ll look at the Fantasy Land spec in its entirety, and go through examples of how we can use the typeclasses within it. However, before we go any further, we need to talk about daggy.

Reductio and Abstract 'em

Oh, hey, stranger! Long time no talk. In case you’re interested, I’ve moved house, job, and company since my last post, hence the hiatus. Sorry! Anyway, speaking of terrible segues, have you ever noticed that you can write every list function with reduceRight?

Snail Shells

Hello, reader mine! Today, I’m on a train back to the north to see my family for the holidays, which gives me the perfect opportunity to write about a conversation I had yesterday: why are terminals so damn unusable?

The Orrery

Hello! Sorry for taking so long to write another post. I’ve been really quite busy looking for a new place to live and a new office to work in, you see. Anyway, instead of adding another post in my introductory theme, I thought I’d show you how this Orrery works! It’s written in Elm, which isn’t supported by GitHub’s highlighter yet, so I’ve modified it a little (my excuse for why the code blocks look a bit naff).

Curry On Wayward Son

Currying is so hot right now in the functional-ish JavaScript community. If you’ve used libraries like Ramda, chances are you’ve had some exposure. Either way, let’s spell it out to be safe:

Peano's Forte

A hundred-ish years ago, long before Pokémon and the Slap Chop, there lived a clever one named Giuseppe Peano, who came up with a neat way to describe the natural numbers (0, 1, 2, 3, ...):

Hello, The Internet

I’m Tom. I write code, which hopefully turns out better than my introductions. Fingers crossed.