type family が injective だと何が嬉しいんだろう（理解してないだけ）
— lotz (@lotz84_) 2017年9月3日

tl;dr
型族を逆にたどって型推論ができるので型を明示的に書かなくて良い場面が増える

GHC8の新しい機能 Injective type families について、名前は前から知ってたもののイマイチどういうものか理解しておらず、Twitterで呟いたところ優しいHaskellerの方々に助けていただき理解することができたので自分でまとめ直してみようと思いこの記事を書いています。

2018/03/11 追記
ryota-ka氏が分かりやすくて実用的な例をまとめてくれたのでこちらも参考にしてください
TypeFamilyDependencies の実用的な例を考える

Type Family

Type family（型族）は型と型の間の関係を記述することができる機能で、型レベル関数だと考えるのがわかりやすいと思います（さらに詳しく知りたい方はこちら What are type families?）。

例えば

type family If c t f where
  If 'True  t f = t
  If 'False t f = f

これは If という型族を定義していて、挙動は見たまんまですが一つ目の型引数に'Trueが来ると二つ目の型引き数の型となり、'Falseが来ると三つ目の形引き数の型となります。

以下は型レベル自然数Natを定義して最小値を求めるMinという型レベル関数を実装した例です。

data Nat = Z | S Nat

type family Min (n :: Nat) (m :: Nat) where
  Min Z m = Z
  Min n Z = Z
  Min (S n) (S m) = S (Min n m)

この型レベル関数 Min を使えば以下のような型レベルで長さの情報を持つVectorに対して

data Vector (n :: Nat) a where
  Nil :: Vector Z a
  Cons :: a -> Vector n a -> Vector (S n) a

instance Show a => Show (Vector n a) where
  show Nil         = "Nil"
  show (Cons a va) = show a ++ ":" ++ show va

型レベルで長さの違う２つのVectorのzipを取る関数vzipのようなものを定義することができます。

vzip :: Vector n a -> Vector m b -> Vector (Min n m) (a, b)
vzip Nil          Nil          = Nil
vzip (Cons _ Nil) Nil          = Nil
vzip Nil          (Cons _ Nil) = Nil
vzip (Cons a va)  (Cons b vb)  = Cons (a, b) (vzip va vb)

実際に試してみましょう

> va = Cons 1 (Cons 2 (Cons 3 Nil))
> :t va
va :: Num a => Vector ('S ('S ('S 'Z))) a

> vb = Cons 'a' (Cons 'b' Nil)
> :t vb
vb :: Vector ('S ('S 'Z)) Char

> vc = vzip va vb
> :t vc
vc :: Num a => Vector ('S ('S 'Z)) (a, Char)
> vc
(1,'a'):(2,'b'):Nil

ちゃんと vc にも正しく型がついてると思います。
（実はこの例は最初 GHC.TypeLits で定義されている Nat を使って実装しようとしたのですが、Min の当たりで型推論がうまく行かずに諦めました。最初はなんでうまくいかないのかもわからなかったのですが Haskell-jp の Slack で丁寧に教えていただいて大変助かりました）

Type family のいろいろな書き方

Closed type families

type family If c t e where
  If 'True  t e = t
  If 'False t e = e

のような書き方はClosed type familiesとよばれ Type family の書き方の一つです。この書き方は上から順番に評価されるため評価の順番がわかりやすいのと where 句以外で定義ができないというメリットがあります。

Open type families

type family If (c :: Bool) t f

type instance If 'True  t f = t
type instance If 'False t f = f

この様に型族の宣言 type family とその"実装"の定義 type instance を分けて書くこともできます。実は Closed type families のときもそうだったのですが If のカインドは Bool -> * -> * -> * で、 Closed type families の定義だとGHCが自動的にcのカインドを推論してくれていたのですが Open type families は誰でも自由にインスタンスを追加できるためカインドの推論ができません。なので Open type families の宣言では If (c :: Bool) t f という風に c のカインドを明示的に書いています。

Associated type family

型族を型クラスの一部として宣言することもできます。

import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as BS

class MonoFunctor mono where
  type Element mono
  omap :: (Element mono -> Element mono) -> mono -> mono

instance MonoFunctor ByteString where
  type Element ByteString = Char
  omap = BS.map

ByteString はカインドが * なので Functor のインスタンスではありませんがコンテナのような挙動をするのでリストの Functor のような振る舞いを持たせてやろうというのが MonoFunctor の発想です。(参考: mono-traversable)

型クラスの中に宣言されている type Element ... というのが Associated type family です。

MonoFunctor は以下のようにちゃんと動きます。

> import Data.Char (toUpper)
> bs = BS.pack "Haskell"
> omap toUpper bs
"HASKELL"

参考: 9.9.2. Synonym families

Injective type families

さていよいよ本題です。GHC 8.0.1 から TypeFamilyDependencies というGHC拡張が追加されました。これは FunctionalDependencies と同じように型変数間の依存関係を型族の宣言でも明示的に書くことができるようにする拡張です。

例えば以下のような型族を考えてみましょう

type family F a
type instance F Int = Integer
type instance F Float = Double

この F は左辺の型を右辺の型に写す型レベル関数と考えることができますが、逆に右辺の型が分かれば左辺の型が分かるという特殊な性質を持ちます。例えば F a が Double だとわかれば a は Float であり F a が Integer だとわかれば a は Int とわかります。この様に $ f(a) = f(b) \Rightarrow a = b $ となるような性質を単射(Injection)と呼びます。F はまさしく単射な型レベル関数というわけです。

このFを使った以下のような関数を考えてみます

f :: Bounded a => F a -> a
f a = maxBound

無理矢理な例ではありますが F a が与えられた時に a の maxBound を返すという関数です。さっそく使ってみましょう

> f (1 :: Integer)

<interactive>:5:1: error:
    • Couldn't match expected type ‘Integer’ with actual type ‘F a0’
      The type variable ‘a0’ is ambiguous
    • In the first argument of ‘print’, namely ‘it’
      In a stmt of an interactive GHCi command: print it

怒られてしまいました。今 F a は Integer なので F の単射性から a は Int だと分かり Int の maxBound である 9223372036854775807 （環境にもよりますが）が表示されるはずです。しかしコンパイラは F が単射であることを知りません。知らないので F a から a を推論してくれません。
もちろん

> (f :: Integer -> Int) 1
9223372036854775807

のように完全に型を指定してやればうまく動いてくれます。でも気持ちとしては引数の型だけ分かれば動いてほしいですよね。そこで登場するのが TypeFamilyDependencies というGHC拡張です。これを使えば F の定義は以下のように書けます

{-# LANGUAGE TypeFamilyDependencies #-}

type family F a = r | r -> a
type instance F Int   = Integer
type instance F Float = Double

type family F a = r | r -> a この部分がキモで、読んで分かるとおり r(F a) から a が定まるよと書いてあるわけです。まさに単射性を指定してるわけですね。このように定義すれば

> f (1 :: Integer)
9223372036854775807

無事引き数の型だけ指定すれば動いてくれるようになりました。ちなみにFloatはBoundedのインスタンスじゃないので

> f (1 :: Double)

<interactive>:2:1: error:
    • No instance for (Bounded Float) arising from a use of ‘f’
    • In the expression: f (1 :: Double)
      In an equation for ‘it’: it = f (1 :: Double)

こっちは動きません

参考: Injective Type Families for Haskell

Data families

実は今まで見てきた type family や type instance といったものは正確には Synonym families と呼ばれるものでGHCの提供する Type Families の機能の一部です。

data family F a
data instance F Int   = F1 Integer
data instance F Float = F2 Double

この様に data family や data instance と宣言する Data families というものもあります。これは定義を見ると分かるように F1 や F2 という新たな値コンストラクタを生成します。

f :: Bounded a => F a -> a
f a = maxBound

Type Families の時と同様に関数 f を定義すると

> f (F1 1)
9223372036854775807

今度は何のGHC拡張を使わずとも型推論を行ってくれます。これは Data Families が値コンストラクタを新たに生成するため自明に単射の性質が F に備わっているからです。
（この例も Twitter ならびに Slack で教えてもらいました。 Data Families の Synonym Families との違いについてはこちらの StackOverflow が詳しいです。）

今回僕がめちゃくちゃお世話になった Haskell-jp の Slack は以下のリンクからから誰でも気軽に参加できます
https://haskell.jp/signin-slack.html