TypeFamilies
以下の拡張を含む
TypeFamiliesの大まかな構成
table:構成
型族とは
簡単な例
Open, Closed, Associatedの使い分け
具体的な使用ケースの例
長さを持つVector n a型同士を連結する関数append :: Vector n a -> Vector m a -> Vector ??? aをどう定義するか？を考える
率直に考えれば、???の部分はn+mになって欲しいが、それを型でどう表現するか
関連論文
関連
参考
open→associated→closedの流れで解説されてて、それぞれの意義がわかりやすい
openからclosedへの書き換え
ユースケース
依存型とはまた違うのか
アドホック多相と、型クラス、型族のアナロジーを見てたら
ただのパターンマッチとアドホック多相の違いがわからなくなった
型族Add
code:hs
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances, DataKinds #-} data Nat = Zero | Succ Nat
type family Add n m where
Add 'Zero n = n
Add ('Succ n) m = Add n ('Succ m)
code:ghci
:kind Add
Add :: Nat -> Nat -> Nat
:kind! Add
Add :: Nat -> Nat -> Nat
= Add
:t Add -- error
kind!で正規化した型を表示する
code:prelude
:kind! Add (Succ (Succ Zero)) (Succ Zero) -- 2+1
Add (Succ (Succ Zero)) (Succ Zero) :: Nat
= 'Succ ('Succ ('Succ 'Zero)) -- 3
関数で書いた場合のイメージ
code:hs
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ n) m = add n (Succ m)
Natはkind
型族If
code:hs
type family If c t f where
If 'True t f = t
If 'False t f = f
:kind!で型関数を実行できる
open, closed, 型クラス内の流れ
openに焦点を当てる
普通にトップレベルで定義できるが、ユースケースを考えると型クラスと一緒に使われがち
だから型クラスで一緒に書いちゃおうと言うのが、型クラス内の定義のやつ
外部から拡張不可能にしたい場合はclosedで定義する
できることがやや増える
つまり、open→closedな書き換えは常に可能だが、逆は無理 #?? openに定義したが型クラスと併用したいパターンってあるのか #?? closedに定義したやつはどういうふうに使われるのか #?? fun depsは単射性を要請するが、型族はそうでもない
パット見似たようなもののように見えるが、どう使い分けるのか？
両方使ってるやつおるん？？
本当に同じものなのかどうかの確認
wiwinwlhは示唆に富むンゴねえ
FUnctor, Foldable, Traversableの一般化
今から見ようとしている型クラスにtype familyがあったら何を連想できるか？
Representableとか
code:hs
class Functor f => Representable f where
type Log f :: *
index :: f a -> (Log f -> a)
tabulate :: (Log f -> a) -> f a
positions :: f (Log f)
tabulate h = fmap h positions
positions = tabulate id
Genricとか
code:hs
class Generic a where
type family Rep a :: * -> * -- representation of the data a
from :: a -> Rep a x
to :: Rep a x -> a
instanceを定義するときに、type familyを指定する必要がある
型関数の返り値となる型を自由に(?)指定できる
それぞれのインスタンス宣言ごとに、区別された 型コンストラクタが作られるイメージ
上ならinstanceごとに別々のLog A _、Log B _といった型コンストラクタができる
要は、multi paramな型クラスである、と考えたほうがわかりやすいかも
2つ以上の型引数を取る型クラスの表現の仕方としてこの表記がある
定義時の型引数はkindが一致していないといけいないのか
code:hs
type family Add n m where
Add 'Zero n = n -- 'ZeroのkindはNat
Add ('Succ n) m = Add n ('Succ m) -- 'SuccのkindはNat
Add String String = Add Int String -- Stringのkindは*なのでエラー
class内にtype宣言する構文も入る
code:hs
class HasKey a where
type Key a
wrapKey :: Int -> Key a
unwrapKey :: Key a -> Int
参考