# Bunny コードリーディング diary （0.9.0 版）

## 2021-01-19

### Kind Inference

Haskell 2010 の [Section 4.6](https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-970004.6)
をちゃんと読んでみよう。

本節では Kind の推定、つまり、与えられたプログラムに出現する型構築子やクラスのそれぞれについて適切な Kind を計算するために用いられる規則について述べる。

Kind 推定の最初のステップは、データ型、シノニム、および、クラス定義の集合を、
依存グループに分類することである。
これは、4.5 節で述べられている値定義の依存解析とほぼ同様の方法で実現可能である。
たとえば、以下のプログラム片には、データ型構築子 D、シノニム S、および、
クラス C が含まれるが、これらはすべて同一の依存グループに属する：

$$<pre>{
  data C a => D a = Foo (S a)  
  type S a = [D a]  
  class C a where  
      bar :: a -> D a -> Bool
$$}

各グループにおける変数、構築子、および、クラスの Kind は、
型推論と Kind を保った同一化に関する標準的な技法$<fn>{ MP Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1):1–36, January 1995.}
によって決定できる。
たとえば、上の例におけるパラメータ $<verb>{a} は、$<verb>{bar} の型において関数構築子 $<verb>{->} の引数となっており、したがってその Kind は $<verb>{*} でなければならない。さらに、D と S の種は $<verb>{* -> *} でなくてはならず、クラス C
のインスタンスはいずれも Kind $<verb>{*} をもつ。

It is possible that some parts of an inferred kind may not be fully determined by the corresponding definitions; in such cases, a default of ∗ is assumed. For example, we could assume an arbitrary kind κ for the a parameter in each of the following examples:


$$<pre>{
  data App f a = A (f a)  
  data Tree a  = Leaf | Fork (Tree a) (Tree a)
$$}

This would give kinds (κ →∗) → κ →∗ and κ →∗ for App and Tree, respectively, for any kind κ, and would require an extension to allow polymorphic kinds. Instead, using the default binding κ = ∗, the actual kinds for these two constructors are (∗→∗) →∗→∗ and ∗→∗, respectively.

Defaults are applied to each dependency group without consideration of the ways in which particular type constructor constants or classes are used in later dependency groups or elsewhere in the program. For example, adding the following definition to those above does not influence the kind inferred for Tree (by changing it to (∗→∗) →∗, for instance), and instead generates a static error because the kind of [], ∗→∗, does not match the kind ∗ that is expected for an argument of Tree:

$$<pre>{
  type FunnyTree = Tree []     -- invalid
$$}

This is important because it ensures that each constructor and class are used consistently with the same kind whenever they are in scope.




### kiExpr