Obtaining the most general type of a Haskell expression is easy. But how do you figure out the more specialized types which your expression also has?

##### Diagrams

Let's draw a simple balloon using the `diagrams`

library.

```
import Diagrams.Prelude
import Diagrams.Backend.Cairo.CmdLine
diagram :: Diagram B
diagram = circle 1
===
vrule 1
```

I want to make the length of the string configurable.

```
{-# LANGUAGE FlexibleContexts, TypeFamilies #-}
balloon n = circle 1
=== vrule n
diagram :: Diagram B
diagram = balloon 2
```

That was easy, but I don't feel comfortable leaving `balloon`

without a type signature. I'm a Haskell programmer, I need types in order to reason about my programs!

##### The most general type

With the proper flags, GHC warns about the fact that my top-level binding doesn't have a type signature and shows me which type it has inferred for it. I can also easily obtain this information via ghci:

```
> :type balloon
balloon
:: (RealFloat (N a), Semigroup a, Transformable a, Juxtaposable a,
TrailLike a, V a ~ V2)
=> N a -> a
```

Oh my, that's a large context! At least I can see why GHC wanted me to add `FlexibleContexts`

(there is a constraint on `N a`

, which isn't a type variable) and `TypeFamilies`

(`V a`

can evaluate to `V2`

, which means `V`

is probably a type-level function, also known as a type family).

I'd like to use a simpler type if possible. Maybe I can instantiate `a`

to a concrete type?

##### Type defaulting

Since GHC 7.8, one easy way to figure out the concrete type at which an expression is instantiated is to pass it as an argument to a type-hole.

```
-- Found hole ‘_typeof’ with type: Integer -> Double
diagram :: Diagram B
diagram = balloon (_typeof 2)
```

The most general type of `2`

is `Num a => a`

, which can get specialized to `Integer`

or `Double`

or any of a large number of types having a `Num`

instance. The `_typeof`

type hole does not further constrain its argument's type, but the type defaulting rules cause `a`

to be specialized to `Integer`

. Then, `balloon`

's complicated type does constrain its argument's type, and when combined with the requirement to produce a `Diagram B`

, `balloon`

's argument must apparently be a `Double`

. At least, that's what the type-hole's inferred type `Integer -> Double`

seems to be telling us.

Or could it be that `balloon`

accepts a more general type than `Double`

, but the defaulting rules simplify this type to `Double`

before we have the chance to observe this more general type? For example, consider the following silly definition:

```
ignoreFractional :: Fractional a => a -> ()
ignoreFractional x = ()
```

If we use a type hole to query the type of `ignoreFractional`

's argument, we get `Double`

, even though the type of `ignoreFractional`

is more general than that.

```
-- Found hole ‘_typeof’ with type: Integer -> Double
main :: IO ()
main = print $ ignoreFractional (_typeof 42)
```

Let's disable type defaulting, so that it stops skewing our results.

```
default ()
```

Note that the syntax for `default`

is `default (type1, type2, ...)`

, not `default type, type2, ...`

, so the above is disabling type defaulting, not configuring the unit type to be the new default instead of `Integer`

.

Without type defaulting, our type hole is no longer concluding that `ignoreFractional`

's argument must be a `Double`

. It also complains that some type variables are ambiguous, which is fine for now.

```
-- Found hole ‘_typeof’ with type: a1 -> a0
-- Where: ‘a0’ is an ambiguous type variable
-- ‘a1’ is an ambiguous type variable
main :: IO ()
main = print $ ignoreFractional (_typeof 42)
```

More importantly, our type hole still says that `balloon`

's argument must be a `Double`

, so type defaulting did not skew our earlier results after all.

```
-- Found hole ‘_typeof’ with type: a0 -> Double
-- Where: ‘a0’ is an ambiguous type variable
diagram :: Diagram B
diagram = balloon (_typeof 2)
```

##### Evaluating type-level functions

Looking at the most general type of `balloon`

more closely, I think I can figure out how `Double`

was chosen. Ignoring the constraints, the type of `balloon`

is `N a -> a`

. We're imposing `a ~ Diagram B`

, and we've already seen that `diagrams`

likes to use type-level functions. Perhaps `N`

is a type-level function which returns `Double`

when given the input `Diagram B`

?

```
> :kind! N (Diagram B)
N (Diagram B) :: *
= Double
```

Indeed it is. Note the exclamation mark in the `:kind!`

command: that's how I am telling ghci that I want to see the result of the type-level function application, not just the kind of this result.

```
> :help
[...]
:kind[!] <type> show the kind of <type>
(!: also print the normalised type)
```

##### The fully-specialized type

We now know that instantiating `a ~ Diagram B`

specializes `N a -> a`

to `Double -> Diagrams B`

, and that this choice for `a`

satisfies all the constraints. I can finally give a short type for `balloon`

:

```
balloon :: Double -> Diagram B
balloon n = circle 1
=== vrule n
```

I could have obtained this answer more easily by using the type hole to query the type of `balloon`

directly.

```
-- Found hole ‘_typeof’
-- with type: (Double -> Diagram B) -> a0 -> Diagram B
-- Where: ‘a0’ is an ambiguous type variable
diagram :: Diagram B
diagram = (_typeof balloon) 2
```

##### Intermediate types

So far, we have seen two extremes: the most general, most abstract type of an expression, and its fully-specialized, most concrete type. There are other types in between those two extremes, obtained by fixing some parts of the type signature but not others.

For example, I now know what the type of `balloon`

specializes to when I force the return type to be the fully-specialized type `Diagram B`

. In `diagrams`

, the `B`

identifies the backend I have imported at the top of the file. Which part of the specialization is due to the fact that the result is forced to be a `Diagram`

, and which part is due to the fact that I am using the Cairo backend?

An answer to this question would be a type signature of the following form:

```
balloon :: _constraint => _input -> Diagram _backend
```

In which `_constraint`

, `_input`

and `_backend`

would be instantiated so that the resulting type signature would be the most general type which is both a valid type signature for `balloon`

's definition and matches the above form. For example, we know from our previous experiments that `_constraint ~ ()`

, `_input ~ Double`

and `_backend ~ B`

would be valid instantiations. Is there a solution which involves more type variables and fewer concrete datatypes?

##### Proxies and identities

Let's ignore the constraints for now. The problem is now much simpler: we have the most general type `N a -> a`

, we have a shape `input -> Diagram backend`

, and we want to unify those two types. Type unification is GHC's bread and butter, we just need to construct a program whose types will require GHC to unify those two types as part of its ordinary type checking phase.

For example, consider the following restricted identity function:

```
myId :: (input -> Diagram backend)
-> (input -> Diagram backend)
myId = id
```

If we apply `myId`

to `balloon`

, GHC will have to find an instantiation for `input`

and `backend`

or otherwise complain that the call doesn't typecheck.

In order to ask GHC which instantiations it has chosen, we can add an extra parameter whose only purpose is to give us a place to put a type hole.

```
import Data.Proxy
typeof :: Proxy (input -> Diagram backend)
-> (input -> Diagram backend)
-> (input -> Diagram backend)
typeof Proxy = id
-- Found hole ‘_proxy’ with type:
-- Proxy (N backend -> Diagram backend)
query = typeof _proxy balloon
```

So there you go, a type signature of the form `_input -> Diagram _backend`

involving type variables instead of concrete types:

```
balloon :: _constraint => N backend -> Diagram backend
```

We still don't know what those constraints should be, and I don't know how the technique could be generalized to obtain it.

Interestingly, the argument type `N a`

got specialized to `N backend`

, the same type-level function but applied to a different type variable. This makes me think that when `N`

is applied to `Diagram backend`

, the `Diagram`

part is probably stripped off and the result is obtained via the recursive call `N backend`

.

```
> :set -XRankNTypes
> :kind! forall backend. N (Diagram backend)
forall backend. N (Diagram backend) :: *
= N backend
```

Indeed it is.

##### Partial type signatures

With the new support for partial type signatures in GHC 7.10, there is now an easier way for us to discover what `_constraint`

, `_input`

and `_backend`

should be instantiated at. I cannot give the name `_constraint`

to the extra constraint wildcard, but as long as the other wildcards can be named, it's still easy to distinguish which is which.

```
{-# LANGUAGE NamedWildCards #-}
-- Found hole ‘_’ with inferred constraints:
-- (RealFloat (N w_backend),
-- TrailLike (QDiagram w_backend (V w_backend) (N w_backend) Any),
-- Metric (V w_backend),
-- V w_backend ~ V2)
-- Found hole ‘_input’ with type: N w_backend
-- Found hole ‘_backend’ with type: w_backend
balloon :: _ => _input -> Diagram _backend
```

I'm guessing that `QDiagram`

is probably related to `Diagram`

in some way. Is `Diagram`

a type synonym for a more complicated `QDiagram`

type?

```
> :info Diagram
type Diagram b = QDiagram b (V b) (N b) Any
```

Bingo.

##### Analyzing the contribution of the backend

Substituting what GHC found for each hole, alpha-renaming, and unexpanding the `QDiagram`

expression back into its `Diagram`

type synonym, I can now give `balloon`

the following type signature.

```
balloon :: ( RealFloat (N b)
, Metric (V b)
, TrailLike (Diagram b)
, V b ~ V2
)
=> N b -> Diagram b
```

That's still quite a mouthful, but compare with the most general type signature we had inferred for `balloon`

earlier:

```
balloon :: ( RealFloat (N a)
, Juxtaposable a
, Semigroup a
, TrailLike a
, Transformable a
, V a ~ V2
)
=> N a -> a
```

We can see that specializing `a`

to `Diagram b`

has had quite an impact on the constraint. The `Juxtaposable`

constraint has been removed, presumably because there is an `instance Juxtaposable (Diagram b)`

somewhere. The same goes for `Semigroup`

and `Transformable`

. The `TrailLike`

constraint remains, presumably because the instances for that involve a concrete backend, something like `instance TrailLike (Diagram B)`

. The `RealFloat`

and `~ V2`

constraints remain as well, but apply to a different type variable, because `N (Diagram b)`

and `V (Diagram b)`

reduce to `N b`

and `V b`

. Finally, the `Metric`

constraint was added, presumably because one of the instances has it as a context, something like `instance Metric b => Juxtaposable (Diagram b)`

.

We now have a better idea of which constraints are satisfied by the fact that `a`

is a `Diagram`

, and which parts of the constraint depend on the particular choice of backend. More importantly, we have learned about many techniques for querying the various types of an expression, which is very useful when you are relying on types as much as I am to understand an existing Haskell codebase.

## No comments:

Post a Comment