PS

Inductive family of types

(Higher inductive types・・・と言いたいがそれはまた別物らしい。)

Family of inductive types

たとえば、Free monad - PS:

  •  \big( a + F(\mathtt{Free} ^ F(a) ) \to \mathtt{Free} ^ F(a) \big) _ a

は、 \mathtt{Free} ^ F(a) fixed pointとするinitial algebraが族になっているだけ(で問題ない)。

Inductive family of types

一方、free applicativeになると、

  •  a + \underset{b}{\exists} ( F (b \to a) \times \mathtt{FreeA} ^ F (b) ) \to \mathtt{FreeA} ^ F (a)

となっており困ってしまったが、これはendofunctorをobjectと考えて

  •  \big( a  + \underset{b}{\exists} ( F (b \to a) \times \mathtt{FreeA} ^ F (b) ) \big) _ a \Rightarrow \mathtt{FreeA} ^ F

なるinitial algebraと考えればいいだけらしい。つまり、fixed pointは  \mathtt{FreeA} ^ F となる。

実際に、これだけからapplicative functorを作れるのかは分からない。*1

参考文献

*1:primitive recursionではない模様