I wrote a big thread on the company Slack to compare type families: open vs closed vs associated. I also ended up discussing data families, as well, since they are a good complement to type families. I’ll probably edit this further and include it in my book, Production Haskell, but here’s the Slack transcript for now:
An associated type family is an open type family, but with the requirement that
it be defined for any type that’s also an instance of the type class. Consider
the mono-traversable library. We have:
type family Element o :: Type
class MonoFunctor o where
omap :: (Element o -> Element o) -> o -> o
class MonoFoldable o where
ofoldMap :: Monoid m => (Element o -> m) -> o -> m
class (MonoFunctor o, MonoFoldable o) => MonoTraversable o where
otraverse :: (Applicative f) => (Element o -> f (Element o)) -> o -> f o
If we wanted to put Element as an associated type, like:
class MonoFunctor o where
type Element o :: Type
omap :: (Element o -> Element o) -> o -> o
Then we’d be a bit stuck - we need to require class (MonoFunctor o) => MonoFoldable o.
This is a stronger requirement than regular Foldable, and
that’s a problem. Or we define a separate type family on MonoFoldable. But then - what do we use with MonoTraversable?
If we’re desperate to avoid open type families, then we can work around this by having a dummy class that only carries the type family.
class HasElement o where
type Element o :: Type
class (HasElement o) => MonoFunctor o where ...
class (HasElement o) => MonoFoldable o where ...
class (MonoFunctor o, MonoFoldable o) => MonoTraversable o where ...
But “a dummy class that only has a type family” seems obviously worse to me than “a type family” :shrug:
The question: “Should I use an open type family or a closed type family?” has an analog to simpler language features: type classes and sum types.
If you want a closed set, you use a sum type. If you want an open set, you use a type class. So if you’re familiar with the trade-offs there, the trade-offs with open/closed type familes are easier to evaluate
A closed set means you can be exhaustive - “every case is handled.” If you’re
pattern matching on a datakind, like type family Foo (x :: Bool), then you
can know that handling Foo 'True and Foo 'False that you’ve handled all
cases. You don’t have to worry that some user is going to add a case and blow
things up. (Well, you kinda do, because even closed type families aren’t
actually closed, due to stuckness semantics, but, uhhhhh, that’s a bit of very
advanced trickery, talk to csongor if you’re curious)
An open set is a way of allowing easy extensibility. So you’re going to accept something of kind Type or possibly a polymorphic kind variable to allow people to define their own types, and their own instances of these types. For example, if I want to associate a type with a string, I can write:
type family TypeString (sym :: Symbol) :: Type
type instance TypeString "Int" = Int
type instance TypeString "Char" = Char
And that lets me run programs at the type level, that end users can extend.
Much like you can write a type class and end users can extend your
functionality.
But ultimately you need to do something at the value level. Which means you need to take some type information and translate it to the value level. This is precisely what type classes do - they are morally “a function from a type to a value.” We can write a super basic function, like:
typeStringProxy :: Proxy sym -> Proxy (TypeString sm)
typeStringProxy _ = Proxy
But this is still not useful without further classes. The Default class assigns a special value to any type, and we could do something like this:
typeStringDefault :: forall sm. Default (TypeString sm) => Proxy sm -> TypeString sm
typeStringDefault = def @(TypeString sm)
Since associating a type class and an open type family is so common, it’s almost always better to use an associated type unless you know that the type family is going to be shared across multiple type classes.
“So how do you associate a closed type family with values?” That’s a great question. We can do the same trick with Proxy functions:
type family Closed (a :: Bool) where
Closed 'True = Int
Closed 'False = Char
closed :: Proxy b -> Proxy (Closed b)
closed _ = Proxy
But, until we know what b is, we can’t figure out what Closed b is. To pattern
match on a type, we need a type class.
class RunClosed (b :: Bool) where
runClosed :: Proxy b -> Closed b
instance RunClosed 'True where
runClosed _ = 3
instance RunClosed 'False where
runClosed _ = 'a'
I’m going to detour a bit here and mention data families. A data family is like a type family, but instead of allowing you to refer to any type, you have to specify the constructors inline. To take an example from persistent,
data family Key a
newtype instance Key User = UserKey { unUserKey :: UUID }
type UserId = Key User
newtype instance Key Organization = OrganizationKey { unOrganizationKey :: UUID }
type OrganizationId = Key Organization
An advantage of this is that, since you specify the constructors, you can know
the type of Key a by knowing the constructor in use - the value specifies the
type. OrganizationKey :: UUID -> Key Organization.
It looks a lot like an “open type family,” and in fact is completely analogous. But we don’t call them “open data families,” even though that’s an appropriate name for it. It should make you wonder - is there such a thing as a closed data family?
Aaaaaand - the answer is “yes”, but we call them GADTs instead.
The nice thing about an “open data family” is that you can learn about types by
inspecting values - by knowing a value (like OrganizationKey uuid), I can work
‘backwards’ and learn that I have an Key Organization. But, I can’t write a
case expression over all Key a - it’s open! and case only works on closed
things. So this code does not work:
whatKey :: Key a -> Maybe UUID
whatKey k = case k of
UserKey uuid -> Just uuid
OrganizationKey uuid -> Just uuid
_ -> Nothing
Indeed, we need a type class to allow us to write get :: Key a -> SqlPersistT m (Maybe a).
A GADT - as a closed data family - allows us to work from a value to a type, and since it is exhaustive, we can write case expressions on them.
data Key a where
UserKey :: { unUserKey :: UUID } -> Key User
OrganizationKey :: { unOrganizationKey :: UUID } -> Key Organization
If I have this structure, then I can actually write get without a type class.
get :: Key a -> SqlPersistT IO (Maybe a)
get k = case k of
UserKey uuid -> do
[userName, userAge] <- rawSql "SELECT * FROM users WHERE id = ?" [toPersistValue uuid]
pure User {..}
OrganizationKey uuid -> ...
A GADT is ‘basically’ a closed type family that gives you constructor tags for
applying that type family,. If we look at Closed, we can inline this:
type family ClosedTy (b :: Bool) where
ClosedTy True = Int
ClosedTy False = Char
data ClosedData (a :: Type) where
ClosedData :: Proxy b -> ClosedData (ClosedTy b)
-- inlining:
data Closed (a :: Type) where
ClosedTrue :: Proxy 'True -> Closed Int
ClosedFalse :: Proxy 'False -> Closed Char
When we case on a Closed value, we get:
runClosed :: Closed a -> a
runClosed closed =
case closed of
ClosedTrue (Proxy :: Proxy 'True) -> 3
ClosedFalse (Proxy :: Proxy 'False) -> 'a'
I’m going to conclude now, with this distillation: