Tag Archives: types

Anafunctors

This is part four in a series of posts on avoiding the axiom of choice (part one, part two, part three). In my previous post, we considered the “Axiom of Protoequivalence”—that is, the statement that every fully faithful, essentially surjective … Continue reading

Posted in category theory, math, species | Tagged , , , , , , , , , , | Leave a comment

AC and equivalence of categories

This is part three in a series of posts on avoiding the axiom of choice (part one, part two). In my previous post, I explained one place where the axiom of choice often shows up in category theory, namely, when … Continue reading

Posted in category theory, math, species | Tagged , , , , , , , , , | 5 Comments

Unique isomorphism and generalized “the”

This is part two in a series of posts on avoiding the axiom of choice; you can read part one here. In category theory, one is typically interested in specifying objects only up to unique isomorphism. In fact, definitions which … Continue reading

Posted in category theory, math, species | Tagged , , , , , , , , | 8 Comments

Avoiding the axiom of choice, part I

I’m hard at work on my dissertation, and plan to get back to doing a bit of blogging based on stuff I’m writing and thinking about, as a way of forcing myself to explain things clearly and to potentially get … Continue reading

Posted in category theory, math, species | Tagged , , , , , | 17 Comments

Unordered tuples and type algebra

At Hac Phi a few weekends ago (which, by the way, was awesome), Dan Doel told me about a certain curiosity in type algebra, and we ended up working out a bunch more details together with Gershom Bazerman, Scott Walck, … Continue reading

Posted in combinatorics | Tagged , , , , | 7 Comments

Typed type-level programming: status report

A few people have been bugging me (you know who you are ;-) about the current status of the project to allow automatic “lifting” of Haskell data constructors to the type level, to allow for typed type-level programming. I’ve written … Continue reading

Posted in haskell, projects | Tagged , , , , , , | Leave a comment

On a Problem of sigfpe

> {-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators, GADTs #-} At the end of his most recent blog post, Divided Differences and the Tomography of Types, Dan Piponi left his readers with a challenge: In preparation for the next installment, here’s a … Continue reading

Posted in haskell | Tagged , , , , , | 2 Comments

Typed type-level programming in Haskell, part IV: collapsing types and kinds

In Part III, we saw how the current state of the art in Haskell type-level programming leaves some things to be desired: it requires duplicating both data declarations and code, and even worse, it’s untyped. What to do? Currently, GHC’s … Continue reading

Posted in haskell, projects | Tagged , , , , | 28 Comments

Typed type-level programming in Haskell, part II: type families

In my previous post, we saw how multi-parameter type classes with functional dependencies in Haskell allow us to do type-level programming in a logic programming style. (If you’re not clear on why this corresponds to a logic programming style, see … Continue reading

Posted in haskell | Tagged , , , | 5 Comments