haskelltypesghctype-families# Why can't type families/synonyms be partially applied, when we can work around the restriction anyway?

Consider the following `Map`

type function:

```
type Map :: (k1 -> k2) -> [k1] -> [k2]
type family Map f l where
Map _ '[] = '[]
Map f (x : xs) = f x : Map f xs
```

I can then define:

```
type MkPair a = (a, a)
```

and attempt to do the following:

```
type Blah = Map MkPair [Int, Char]
```

but I find out that types synonyms can't be partially applied.

But I can do this slightly more roundabout route:

```
type Mapper :: k1 -> k2 -> Type
data Mapper k1 k2 where
Mapper :: Type -> Mapper k1 k2
type MapF :: Mapper k1 k2 -> [k1] -> [k2]
type family MapF f l where
MapF _ '[] = '[]
MapF ft (x : xs) = MapFT ft x : MapF ft xs
type MapFT :: Mapper k1 k2 -> k1 -> k2
type family MapFT kt k1
data MkPair
type instance MapFT ('Mapper MkPair :: Mapper Type Type) a = (a, a)
type Blah = MapF ('Mapper MkPair :: Mapper Type Type) [Int, Char]
-- This compiles
f :: Proxy Blah -> Proxy '[(Int, Int), (Char, Char)]
f = id
```

I can even do this:

```
data SymMap
type instance MapFT ('Mapper SymMap :: Mapper Symbol Type) a = Proxy a
g :: Proxy (MapF ('Mapper SymMap :: Mapper Symbol Type) ["hello", "world"]) -> Proxy '[Proxy "hello", Proxy "world"]
g = id
```

And all is good.

It seems to me I've subverted the "can't partially apply type synonyms" thing. This transformation seems messy but it's also mechanical, and it's not obvious to me what cases this transformation wouldn't work?

So then I ask, what is the purpose of the restriction of not being able to partially apply type synonyms/families, if one can just work around it by moving your synonym into a type family?

Solution

Type families can't be partially applied because it breaks type inference. In GHC, the equality `f a ~ g b`

is equivalent to `f ~ g`

and `a ~ b`

. That is no longer the case if `f`

and `g`

are allowed to be type families. You can work around it by distinguishing two kinds of type-level applications, but the use cases probably weren't as clear as they are now at the time when type families were introduced. See also Higher-order type-level programming in Haskell.

That transformation to work around the lack of partial application is called defunctionalization.

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code