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"
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