Profile

Cover photo
Dan Doel
Works at Capital IQ
Attended Case Western Reserve University
Lives in Somerville, MA
202 followers|61,151 views
AboutPostsPhotosYouTube

Stream

Dan Doel

Shared publicly  - 
 
This guy makes the best videos.
1
Add a comment...

Dan Doel

Shared publicly  - 
 
Very generalized categories of structures, free and cofree things in Haskell. Hope you like Kan extensions.
In the last couple posts I've used some 'free' constructions, and not remarked too much on how they arise. In this post, I'd like to explore them more. This is going to be something of a departure from the previous posts, though, since I'm not going to worry about thinking precisely about ...
4
Add a comment...

Dan Doel

Shared publicly  - 
 
Speaking with +Edward Kmett about some operad stuff he's been doing caused me to realize a new way of seeing that all the GADT stuff in Haskell is not really dependent types.

My usual go-to example is functions. Whenver people use GADTs and indexing to fake dependent types, they think about data types. And those are amenable to faking (though it's often not pleasant) because, well, indexed data types are data. But functions are wired in, and there's really no good way (that I know of) to represent singleton subtypes of function spaces using GADTs, at least if you want it to look remotely similar to dependent types.

However, I came to the realization that it isn't really even adequate for data types, because the semantics of the type level are different than those of the value level. For instance, I wrote some stuff recently about how (finite) lists aren't the free monoid in Haskell. But Haskell's type level is expected to behave more like a total language, so finite lists are the free monoid at the type level.

And even though we have all kinds of automatic lifting now, the semantics don't actually line up. The 'faking it' procedure is that to have 'dependent types' involving T, you lift T to the type level, create T' :: T -> *, and maybe recover T by working with ∃(t :: T). T' t. But this construction actually isn't the same as having types that depend on your original T (for Haskell), because it is actually constructing the finitary version of T. There are even certain rules for working with existentials that ensure this is the case.

The short version is that reasoning about the lifting of your data type doesn't mean you're actually reasoning about the original value level type, just about a corresponding object with an analogous definition.
6
Michael Shulman's profile photoUrs Schreiber's profile photo
10 comments
 
I see. Well, then it only remains to hope that Agda eventually attracts a larger community of real-world programmers. Should make for some interesting synergy effects.
Add a comment...

Dan Doel

Shared publicly  - 
 
More thoughts about sets vs. domains with a lot of digression on how traversals are related to free applicatives.
Last time I looked at free monoids, and noticed that in Haskell lists don't really cut it. This is a consequence of laziness and general recursion. To model a language with those properties, one needs to use domains and monotone, continuous maps, rather than sets and total functions (a ...
2
Add a comment...

Dan Doel

Shared publicly  - 
 
I saw a youtube comment complaining that a two Michelin star rated chef in the video said, "English feta cheese," while feta is a Greek cheese, and it reminded me of this.
Paul Chiusano. Functional programming, UX, tech, econ. Twitter • GitHub • LinkedIn • RSS. Consulting services. I offer Scala and FP consulting services. If you're interested in working together, please contact me. About my book. My book, Functional Programming in Scala, uses Scala as a vehicle ...
1
Add a comment...

Dan Doel

Shared publicly  - 
 
Scott obviously likes math, because he can do 497 × 35 in his head!
1
Add a comment...

Dan Doel

Shared publicly  - 
 
French onion soup.

Took a lot of prep time, but it was a pretty good payoff.
2
Dan Doel's profile photo
 
Looks like google's technology for determining the ingredients of food in pictures isn't very good yet.
Add a comment...
In his circles
70 people
Have him in circles
202 people
Aaron Seigo's profile photo
Anthony Enache's profile photo
James Cook's profile photo
sandra Shola's profile photo
Carlos López-Camey's profile photo
Dustin Getz's profile photo
Bas van Dijk's profile photo
Kyra Alex's profile photo
Benjamin Sun's profile photo

Dan Doel

Shared publicly  - 
 
Reason #12 for having proper tail calls: it makes garbage collection more precise.

Over at

    https://bitbucket.org/ermine-language/ermine-writers

we have some code for generating Excel files (edit: apparently we don't; we just have generators for other stuff. You'll just have to take my word for what the Excel version looks like), and it turns a fairly declarative specification of the file into effectful procedures that generate the file; T -> U with a side effect. You can combine multiples of these by running them in sequence; something like:

    \t -> f t ; g t

However, there's a problem (if your language implementation doesn't handle this right). In the code above, once we're in g, we're clearly done with f, and it and all the things it transitively references could be garbage collected (at least as far as we're concerned). But without the call to g eliminating the stack frame of our lambda, the reference to f is still live, and it has to stick around.

This is also a good reason for the compiler to CPS your code (or do something similar; the STG used in GHC is nearly in A-normal form for instance), so that you can handle cases like:

    \t -> f t ; g t ; h t

Once we've jumped from f into the continuation {g t ; h t}, f is no longer live. But without this sort of implementation, building up structure using first class functions and closures is expensive.
4
Add a comment...

Dan Doel

Shared publicly  - 
 
I think this might be a good video to show programmers who are struggling with learning Haskell, monads, category theory, etc. There are, naturally, a lot of parallels between that stuff and learning to ride a backwards bicycle after already knowing how to ride a normal one.

It also kind of illustrates +Brent Yorgey's monad tutorial fallacy. When people's brains snap over to finally understanding, they tend to think it was the last example or analogy they read that did it, when it was actually the period of repeated struggling, and everything eventually snapping into place is just how understanding works in general.
6
Shae Erisson (shapr)'s profile photoAlbert Lai's profile photo
2 comments
 
Like I say, the best calculus textbook is the third one you read.
Add a comment...

Dan Doel

commented on a video on YouTube.
Shared publicly  - 
 
Eagerly awaiting the more faithful fan edit, where Bilbo gets hit in the head by a rock, followed by 3 hours of blank video. Then Bilbo wakes up and goes home.
2
Add a comment...

Dan Doel

Shared publicly  - 
 
Deja vu.
2
Erik de Castro Lopo's profile photo
 
Had a scene very much like that here in Sydney a week or two back.
Add a comment...

Dan Doel

Shared publicly  - 
 
Today I was again reminded why having proper tail calls in your language is important (and why optimization of tail recursion doesn't cut it), and felt like ranting a bit. I'm going to use Haskell syntax, but pretend it's a language that's strict (hence the () ->) and only has tail recursion optimization.

We were seeing a stack overflow in some of our code, and tracked it down to some stream processing we were using. The processors looked something like:

    data SP k r
      = Done
      | Emit r (() -> SP k r)
      | forall e. Await (k e) (e -> SP k r) (() -> SP k r)

With this you can make regular and branching processors:

    type Process i o = SP ((->) i) o
    newtype (f + g) a = Sum (Either (f a) (g a))
    type Tee i j o = SP (( ->) i + ( ->) j) o

and you might want to pipe together Processes and Tees:

    tee :: Process i i' -> Process j j' -> Tee i' j' o -> Tee i j o
    tee _ _ Done = Done
    tee l r (Emit o next) = Emit o $ \() -> tee l r $ next()
    tee l r (Await req s f) =
      either
        (\kl -> case l of
          Done -> tee l r $ f()
          Emit i next -> tee (next()) r (s $ kl i)
          Await reql sl fl -> ...)
        (...)
        req

Hopefully this is pretty straight forward. If the branch processor is done, so is the composition; if the branch emits a value, so does the composition; if the branch needs a value, it queries the appropriate single stream being fed in.

But, this code has a problem: tee is not tail recursive. In some cases this is appropriate, because Emit is postponing recursive calls to tee to when more structure is demanded. Recursion is broken by constructor emissions, and the onus is on the consumer to not overflow the stack. But, in the case where we have input to feed into a requesting branch stream, the non-tail recursive cases will break the optimization that prevents a stack overflow from happening. So we are forced to write some boilerplate that separates the tail recursion from the non-tail recursion:

    annihilate l r Done = Done
    annihilate l r (Emit o next) = Emit o $ \() -> tee l r $ next()
    annihilate l r (Await req s f) =
      either
        (\kl -> case l of
          Done -> annihilate l r $ f()
          Emit i next -> annihilate (next()) r (s $ kl i)
          ...)
        (...)
        req

    tee l r t = annihilate l r t

annihilate calls itself in the tail positions and tee in the non-tail positions, so the compiler can figure out how to generate code that actually works.

But wait! annihilate still doesn't work. Why? Well, we've used a function for control flow; either. But this means that the entire rest of the Await case is not in the tail position, so neither are all our calls to annihilate. So we must inline the definition of any such helper functions until our control flow consists only of blessed primitive constructs that the compiler considers eligible for tail recursion optimization.

In other words, lack of proper tail calls requires programmers to write boilerplate, and makes user-defined control flow abstractions less useful.
4
Add a comment...
People
In his circles
70 people
Have him in circles
202 people
Aaron Seigo's profile photo
Anthony Enache's profile photo
James Cook's profile photo
sandra Shola's profile photo
Carlos López-Camey's profile photo
Dustin Getz's profile photo
Bas van Dijk's profile photo
Kyra Alex's profile photo
Benjamin Sun's profile photo
Work
Occupation
Software Engineer
Skills
Haskell, Type Theory, Category Theory, Agda, Scala
Employment
  • Capital IQ
    Software Engineer, 2011 - present
Places
Map of the places this user has livedMap of the places this user has livedMap of the places this user has lived
Currently
Somerville, MA
Previously
Cambridge, MA - Maineville, OH - Cleveland, OH
Links
YouTube
Contributor to
Story
Introduction
Why don't you try making four beats a day for two summers?
Education
  • Case Western Reserve University
    Computer Science, 2001 - 2005
Basic Information
Gender
Male