TypeFamilyDependencies
from Type Family
GHC拡張
#WIP
ただのTypeFamiliesだけでは単射になっていない
から、どんな問題が起こる #??
https://ryota-ka.hatenablog.com/entry/2018/03/10/205817
この拡張を有効にしていないと怒られるケース
そこでこの拡張を使うことで、単射を強制できる
MultiParamTypeClassesとFunctionalDependenciesの関係に似てる #??
逆に、type family depを付けずに、type familyを使う利点はあるの #??
言い方を変えれば、常にtype family depを有効にしているせいで生じる問題はあるの?
この拡張は何?単射であることを強制するだけ?
Data Familyとの使い分けは #??
type synonymに対してはType Family Depsの拡張を使うとか?
複雑やなーmrsekut.icon
/mrsekut-private/型族#6113d4a51982700000f1a4ae
単射な例
code:hs
type family F a
type instance F Int = Integer
type instance F Float = Double
これは普通のTypeFamiliesでの記述
TypeFamilyを型レベル関数として見るをすればわかりやすい
$ f(a)=f(b) \Rightarrow a=bが成り立っているのがわかる
右辺を見れば、左辺を特定できる
F aがIntegerだとわかれば、aはIntだとわかる
こう書く
code:hs
{-# LANGUAGE TypeFamilyDependencies #-}
type family F a = r | r -> a
type instance F Int = Integer
type instance F Float = Double
Data Familyでも同様の結果を得られる
code:hs
data family F a
data instance F Int = F1 Integer
data instance F Float = F2 Double
F1, F2のような値コンストラクタを作るので、自明に単射になる
https://qiita.com/lotz/items/6c038698c8f04f57113a
の読みメモ
injective type families
https://gitlab.haskell.org/ghc/ghc/-/wikis/injective-type-families
https://ryota-ka.hatenablog.com/entry/2018/03/10/205817
https://twitter.com/lotz84_/status/904270563794763777
http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones_eisenberg_injectivity_extended.pdf