Profile

Cover photo
Dan Doel
Works at Capital IQ
Attended Case Western Reserve University
Lives in Somerville, MA
219 followers|66,814 views
AboutPostsPhotosYouTube

Stream

Dan Doel

Shared publicly  - 
 
Someone mentioned to me after I wrote the adjoint triples blog post that the colim ⊣ const ⊣ lim triple can actually be seen as part of the cohesion adjoint quadruple, where the quadruple would have a right adjoint to lim (I think).

So, I fooled around, and figured out that the analogue of that triple in Haskell (or really, a total version thereof) actually extends into an adjoint quintuple, with a right adjoint to lim (forall) and a left adjoint to colim (exists). At least, it works for the co- and contravariant endofunctor cases---I didn't bother thinking about quantifying over higher-kinded types and whatnot.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 ...
1
Urs Schreiber's profile photoDan Doel's profile photoGershom B's profile photo
8 comments
 
Here is the freely available version of the adjoint quintuple paper, from Rosebrugh's website: http://www.mta.ca/~rrosebru/articles/accs.pdf
Add a comment...

Dan Doel

Shared publicly  - 
 
I haven't bothered reading up on 5th edition D&D, so I don't know how good or bad it's supposed to be. But I imagine it's a bad sign that they're reprinting 2nd edition.
1
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 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...
Have him in circles
219 people
Daring Lizzie's profile photo
Lone Ffog's profile photo
Rebecca Doel's profile photo
Shayly Mcdonnell's profile photo
Gustavo Adolfo Gonzalez Ojeda's profile photo
Alan Jeffrey's profile photo
Henk Poley's profile photo
Edward Yang's profile photo
Alin Velciu's profile photo

Dan Doel

Shared publicly  - 
 
Fun with adjoint triples and the (co-)Yoneda lemma.
A common occurrence in category theory is the adjoint triple. This is a pair of adjunctions relating three functors: F ⊣ G ⊣ H F ⊣ G, G ⊣ H. Perhaps part of the reason they are so common is that (co)limits form one: colim ⊣ Δ ⊣ lim. where Δ : C -> C^J is the diagonal functor, ...
6
3
Urs Schreiber's profile photoDan Doel's profile photo
16 comments
 
The context was that this is a type theory where there are modal pi types that are not (or do not appear to be) reducible to a unary modality on types, and I was asking whether this was something that came up elsewhere, like in the other research on modal type theory you pointed to.

But from trying to explain it, I'm coming more to the conclusion that the modal part is unary, and the fact that it's baked into pi types is a quirk of the theory. It's not actually some kind of binary modality like I had thought. Just separating the modality from the pi type while preserving the behavior is difficult.
Add a comment...

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  - 
 
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).
7
3
Gershom B's profile photoDan Doel'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...
People
Have him in circles
219 people
Daring Lizzie's profile photo
Lone Ffog's profile photo
Rebecca Doel's profile photo
Shayly Mcdonnell's profile photo
Gustavo Adolfo Gonzalez Ojeda's profile photo
Alan Jeffrey's profile photo
Henk Poley's profile photo
Edward Yang's profile photo
Alin Velciu'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