Inside 206-105

Existential Pontification and Generalized Abstract Digressions

Denotational Semantics

No one expects the Scott induction!

Recursion is perhaps one of the first concepts you learn about when you learn functional programming (or, indeed, computer science, one hopes.) The classic example introduced is factorial: fact :: Int -> Int fact 0 = 1 -- base case fact n = n * fact (pred n) -- recursive case Recursion on natural numbers […]

ω: I’m lubbin’ it

Today we’re going to take a closer look at a somewhat unusual data type, Omega. In the process, we’ll discuss how the lub library works and how you might go about using it. This is of practical interest to lazy programmers, because lub is a great way to modularize laziness, in Conal’s words. Omega is […]

Getting a fix on fixpoints

Previously, we’ve drawn Hasse diagrams of all sorts of Haskell types, from data types to function types, and looked at the relationship between computability and monotonicity. In fact, all computable functions are monotonic, but not all monotonic functions are computable. Is there some description of functions that entails computability? Yes: Scott continuous functions. In this […]

Errata for gin and monotonic

Between packing and hacking on GHC, I didn’t have enough time to cough up the next post of the series or edit the pictures for the previous post, so all you get today is a small errata post. The full list diagram is missing some orderings: ★:⊥ ≤ ★:⊥:⊥ and so on. In usual denotational […]

Gin and monotonic

Gin, because you’ll need it by the time you’re done reading this. Last time we looked the partial orders of values for data types. There are two extra things I would like to add: an illustration of how star-subscript-bottom expands and an illustration of list without using the star-subscript-bottom notation. Here is a triple of […]

Hussling Haskell types into Hasse diagrams

Values of Haskell types form a partial order. We can illustrate this partial order using what is called a Hasse diagram. These diagrams are quite good for forcing yourself to explicitly see the bottoms lurking in every type. Since my last post about denotational semantics failed to elicit much of a response at all, I […]

How I Learned to Stop Worrying and Love the ⊥

An extended analogy on the denotational and game semantics of ⊥ This is an attempt at improving on the Haskell Wikibooks article on Denotational Semantics by means of a Dr. Strangelove inspired analogy. The analogy. In order to prevent Brigadier General Jack D. Ripper from initiating a nuclear attack on Russia, the Pentagon decides that […]