Profile

Cover photo
Dan Doel
Works at Capital IQ
Attended Case Western Reserve University
Lives in Somerville, MA
209 followers|62,712 views
AboutPostsPhotosYouTube

Stream

Dan Doel

Shared publicly  - 
 
On the topic of bugs in Google products (last one being their android music player)....

The gmail spam filter is terrible these days. I have to regularly check my spam folder, because it has non-spam messages almost every week. I had to modify my haskell-cafe rule to skip the spam filter, because it was erroneously marking so many of those as spam (and I doubt it's commentary on the quality of that list). It's off target on most other mailing lists, too.

A google search for "google spam filter sucks" reveals that Linus Torvalds discovered this recently, too, after gmail started marking 30% of his Linux kernel mailing list traffic as spam.

Even better, it regularly marks Google's own alert messages about logins from new devices as spam.
3
Urs Schreiber's profile photoDan Doel's profile photo
2 comments
 
Yeah, I found that first post, at least.

Unfortunately, I've just been getting moderately poor performance for a year or so, instead of extremely poor performance that is fixed in 10 days.
Add a comment...

Dan Doel

Shared publicly  - 
 
This weekend, for the Boston Haskell hackathon, a bunch of people who pay more attention to homotopy type theory than I do are in town. So I've been looking at the notes for cubical type theory to catch up some (on the parts that are relevant to my interests).

I can't really claim to understand them well. Some of it is written in typing rules, but some of the notation used is unexplained, and seems to expect you to understand it via intuition about categorical models that I don't have a good understanding of. But, eventually I came to something that explained a big gap in my understanding. The question is, "if I know eq : T = U, and I have P(T) how do I get P(U) if eq can have computational content and must apply functions at all the right places?" And the answer in cubicaltt is that some operations are defined by induction on types.

This isn't that surprising, because observational type theory did the same thing. However, a big difference occurs to me. Observational type theory went to great lengths to ensure that equality was computationally irrelevant. And this presumably ensures that the things defined by induction on types don't matter when you run your program. But the whole point of cubicaltt and the like is that equality is not only relevant, but has non-trivial content.

So the question is, can you erase types (or terms of type U if you prefer)? And the immediate answer that occurs to me is, "no." This isn't actually that novel either. It is related to the question of whether you can statically resolve all dictionary passing for type classes in Haskell. JHC, for instance, implements type classes by case analysis on (representations of) types, and so it cannot erase all of them statically. But it might not be immediately obvious that internalizing the, "everything respects weak equivalence," (meta) fact would have a similar effect.
2
Gershom B's profile photoDan Doel's profile photoroux cody's profile photo
14 comments
 
+Dan Doel Ah I see, I was thinking more along the lines of "dependency erasure", which is less apropos.
Add a comment...

Dan Doel

Shared publicly  - 
 
Wrote down my arguments about why unsafeInterleaveIO isn't actually as bad as its reputation suggests. With digressions about referential transparency and purity, in case you want to use terminology exactly the same way I do.
One area where I'm at odds with the prevailing winds in Haskell is lazy I/O. It's often said that lazy I/O is evil, scary and confusing, and it breaks things like referential transparency. Having a soft spot for it, and not liking most of the alternatives, I end up on the opposite side when the ...
6
1
John Lato's profile photoNeil Mitchell's profile photoDan Doel's profile photoGershom B's profile photo
3 comments
 
+Neil Mitchell
Yeah. It's Ed's blog, and a while back he invited me to write guest posts, because I wasn't really interested in making my own. But no one ever informed the planet haskell folks (or whatever is necessary to display something other than Ed's name).
Add a comment...

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.
5
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

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...
Have him in circles
209 people
Timothy Braje's profile photo
Alin Velciu's profile photo
Alex Lang's profile photo
Larry Diehl's profile photo
Eduard - Gabriel Munteanu's profile photo
Josh Cough's profile photo
Tom Moertel's profile photo
Mikolaj Konarski's profile photo
Edward Kmett's profile photo

Dan Doel

Shared publicly  - 
 
Notes on notes on cubical type theory

After a few days of looking at these notes, the implementation, and some random background material, I think I have a rough understanding of what's going on in cubical type theory. I've heard that there's some confusion amongst people who aren't the implementers as to what's going on, and it's fairly easy to understand why. Certain notation in the notes is both non-standard and completely unexplained. And some (I think) important subtleties with the rules are also unexplained.

Fortunately, I've implemented and used enough type theories that I can go read the implementation and figure out what the notation is actually supposed to mean (in some cases). I'm not sure if this puts me in a small, advantaged subset of people, or if the stuff I understand is trivial and the 'confusion' is over bigger issues. But, here are my notes on how to understand the notes, in case it helps anyone.

First some background. Cubical type theory is based on cubical sets, which are used in category theory as a model for homotopy. These are in turn based on the cube category, which is a category whose objects are n-dimensional cubes. The 0 cube is a point, the 1 cube is a line segment, the 2 cube is a square, etc.

Cubical sets are presheaves on the cube category. So A : Cube^op -> Sets. This should be thought of as taking the 0-cube to the type A, the 1-cube to identities between values of A, the 2-cube to identities between identities, etc.

So, the core idea behind cubical type theory is that we add the 1-cube, to the formalism. This can be thought of as an interval type 𝕀, which has two elements that are identical to each other (but only propositionally). Functions f : 𝕀 -> A are then like two elements of A together with a proof that they are identical.  That is, 𝕀 -> A is like (Σ x y : A. Id A x y), which is the 1-cube portion of the cubical set for A. And we construct higher cubes by iterating the 𝕀 ->. This is like currying the product of intervals that form higher cubes.

The other angle is that when we have 𝕀 -> A, this can be flipped around to get back dependent types, because it can be used in slice categories. So, any particular t : 𝕀 -> A corresponds to an element in the fiber above its two values. So there is a corresponding eq : Id A (t 0) (t 1). This is what cubical type theory actually uses; there's a special lambda that lets us go from "Γ , i : 𝕀 ⊢ t(i) : A" to "Γ ⊢ <i> t(i) : Id A (t 0) (t 1)".

Now, onto the actual notes on the notes.

The first thing to know is the notation A(i0). This is used when A is defined in a context including i : 𝕀, and it means to substitute 0 in for i in A. This is one of the things that isn't explained anywhere in the notes, but reading the code makes it pretty clear that's the intention.

Another thing to know is that the above lambda is not the fully general formulation of things, I think. The code written in cubicaltt the language references an IdP type, and defines the normal identity in terms of it. This is used for type families fibred over the interval, which is written in the notes like "Γ, i : 𝕀 ⊢ A". This makes IdP actually a sort of heterogeneous equivalence type, mediated by a specified equivalence of types, and can be thought of as Πi:𝕀.A(i) instead of 𝕀 -> A (perhaps this is where the name IdP comes from? P for Π?). You can mimic this (I think) in something like Agda by defining a type:

    IdP {A} {B} (AB : A == B) (x : A) (y : B) = subst id AB x == y

But needless to say, it seems significantly more convenient to work with in the cubical rules. This is something of a disconnect between the implementation and the rules, I should note. The implementation works with typing judgments as things being of type U, and appears to let you form functions 𝕀 -> U, because judgments are behind the scenes in an implementation. This is a slight mismatch, but it's pretty common when moving from typing rules to a computer implementation.

One of the reasons why this comes up is the very last set of rules about "glueing" (sic). Glue is (part of) how univalence is added to the theory; it lets you demonstrate an isomorphism (up to identity) and get an identity. The thing to note here is that there are two "glue"s. One is term-level, and the other is type-level. The notes write them almost identically, but I'll write the type level one with a capital. Anyhow, types built with Glue are an example of something that is fibred over the interval. You demonstrate an Iso(T, A), and using Glue with that lets you build a type family that will reduce to T when i = 1, and A when i = 0. And glue lets you move elements along that isomorphism, so it lets you create identity types that match up corresponding elements of the isomorphic types.

The last very cryptic thing is "formulas" in the context. There is pretty much no explanation for them, but they are used in Glue and comp. If you read some cubicaltt programs, you'll see that they look completely different there, like "i = 0". So what I think they are is a way to do case analysis on interval elements in a controlled way. The rules for using them ensure that you can only 'branch' in ways such that the result of each branch will be judged equal in a joint context. The formula 'i' corresponds to the case 'i = 1' and the formula '1 - i' corresponds to the case 'i = 0'. The weird "u_{φ,ψ}v" notation is a way to collect up two branches into one expression, and it's a value that reduces to u when φ = 1 and v when Ψ = 1.

The last problematic thing about formulas is how you even derive things with them in the context. I think one important thing that isn't explained is that you can probably weaken by formulas in some way. Like 'Γ ⊢ a : A' yields 'Γ, φ ⊢ a : A', possibly with side conditions. Or perhaps 'Γ ⊢ a : A' yields 'Γ, 1 ⊢ a : A'. Structural rules like this aren't given, though.

The last thing to understand is comp, but I already covered that in my last post. However, my explanation there might not give the clearest idea of how things work exactly. Namely, a 'x = y -> P x -> P y' type substitution is not fundamental in cubical type theory. To get that sort of substitution, you first prove 'P x = P y' and then use an operation 'comp' that takes 'A = B' to 'A -> B'. So, you never need to inspect a function like P, you only need to inspect its application to things. You can build expressions that demonstrate (effectively) 'P x = P y' in completely abstract contexts, using (interval) lambda and application, and induction on types is used to figure out how those lambda terms need to compute on values.

The last notational bit about comp is that it binds a variable. The hypotheses of comp formation include 'i : 𝕀' in the context, and then 'comp^i' binds i for its subexpressions. But 'fill', which is defined in terms of comp, and uses a similar notation, does not bind its superscript.

I think that's about it. With the above, I think it's possible to get a feeling for the cubicaltt notes on a sort of operational level (figuring out why the computation rules for comp are what they are is then the difficult part). Whether it's any good as a model of homotopy stuff, I can't say, because I know very little about homotopy/topology. But maybe it can help some other folks like me who are more interested in the computational aspects than a syntactic theory of a branch of mathematics (or maybe it will help the latter folk, too; who knows).
6
3
Dan Doel's profile photoGershom B's profile photoroux cody's profile photoBoris Borcic's profile photo
2 comments
 
Ah. So it's related to the encoding in something like Agda, I guess.

I realized that I said one thing here that didn't make sense. Namely, I said that we could construct 'P x = P y' from 'x = y' in an abstract context. However, there is no type 'P x = P y', because U is not a type in the rule system, so 'Id U' isn't either (the implementation appears to be different; in fact, it appears to have U : U, which is going to be a problem unless they've hidden universe indexing in there).

If you read about OTT, you'll see that they actually have two identity types. One is identity of types, and the other is identity of terms. The Id type in the cubical rules is term identity, and there is no type identity type, it is just left implicit in the rules as judgments like 'i : I ⊢ A'.

The semantics of term identity on A is I -> A, and we can project out the points at either end. But with type identity, we can not just project out the types at either end, but functions mediating between those two types. So, the formula rules let us demonstrate how those functions work by cases on the intervals involved (note, that 'u' element in the comp rule is an identity on A, because it's under an interval context; so it explains which values at either end of the type equality are related). And comp allows applying those functions to go from A(0) to A(1).

That kind of explains how fill works, too. You have some identities explaining how things in a square work, and you use comp to explain how to connect those together to get the missing identities.
Add a comment...

Dan Doel

Shared publicly  - 
 
Sometimes I wonder if Google will ever decide to make the playlist/"queue" in their music player (for android) not horribly buggy.
1
Dan Doel's profile photoShae Erisson (shapr)'s profile photo
3 comments
 
Wow, I've seen one or two of those, but I thought it was just a minor problem, but I assemble all my playlists on the web interface.
I do wish they had a query API, I like to figure out what music works for me when, and try to organize up more of the same.
Add a comment...

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

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...
People
Have him in circles
209 people
Timothy Braje's profile photo
Alin Velciu's profile photo
Alex Lang's profile photo
Larry Diehl's profile photo
Eduard - Gabriel Munteanu's profile photo
Josh Cough's profile photo
Tom Moertel's profile photo
Mikolaj Konarski's profile photo
Edward Kmett'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