依存型
aumy.icon 自信ない
型が引数に依存できるような型システム
どういうことか?
式が引数に依存する例
code:lean
fun (n : Nat) => n + 1
関数のbodyにあたる式 n + 1 は引数 n に依存している
Type -> Type -> Type × Type
(α : Type) -> α -> List α -> List α
型が(型)引数に依存する例
Leanだと値レベル引数と区別された型引数という概念があるわけではない code:lean
fun (α : Type) (head : α) (tail : List α) => List.cons head tail
このとき head tail の型として引数 α が登場している