依存型とは？
いぞんがた
値に応じて変わる型の仕組みだよ。
『依存型』とは型の中に値の情報も入れられる高度な仕組みでリストの長さを型で保証できるよ。
つかいかた・れいぶん
Idrisでは長さ3のリストと長さ5のリストを型レベルで区別できるよ。
このことばを シェア
さいごの こうしん: