私の質問を意味のあるものにするために、背景を説明する必要があります。
a他のパラメーターや戻り値が に依存する型を持つ関数の引数の存在と型を推測できる依存型付き言語があれば便利だと思いますa。私が設計している言語で次のスニペットを検討してください。
(* Backticks are used for infix functions *)
def Cat (`~>` : ob -> ob -> Type) :=
sig
exs id : a ~> a
exs `.` : b ~> c -> a ~> b -> a ~> c
exs lid : id . f = f
exs rid : f . id = f
exs asso : (h . g) . f = h . (g . f)
end
2 つの (確かに、不当な) 仮定を行うと、次のようになります。
- 明示的に提供された情報から推測できない依存関係が存在してはなりません。
defすべての自由変数は、またはを使用して導入された最後の識別子の暗黙の引数に変換する必要がありますexs。
上記のスニペットは、次のものと同等であると解釈できます。
def Cat {ob} (`~>` : ob -> ob -> Type) :=
sig
exs id : all {a} -> a ~> a
exs `.` : all {a b c} -> b ~> c -> a ~> b -> a ~> c
exs lid : all {a b} {f : a ~> b} -> id . f = f
exs rid : all {a b} {f : a ~> b} -> f . id = f
exs asso : all {a b c d} {f : a ~> b} {g} {h : c ~> d}
-> (h . g) . f = h . (g . f)
end
これは、次の Agda スニペットとほぼ同じです。
record Cat {ob : Set} (_⇒_ : ob → ob → Set) : Set₁ where
field
id : ∀ {a} → a ⇒ a
_∙_ : ∀ {a b c} → b ⇒ c → a ⇒ b → a ⇒ c
lid : ∀ {a b} {f : a ⇒ b} → id ∙ f ≡ f
rid : ∀ {a b} {f : a ⇒ b} → f ∙ id ≡ f
asso : ∀ {a b c d} {f : a ⇒ b} {g} {h : c ⇒ d} → (h ∙ g) ∙ f ≡ h ∙ (g ∙ f)
明らかに、2 つの不当な仮定により、多くのタイピングの手間が省けました!
注:もちろん、このメカニズムは、元の仮定が保持されている場合にのみ機能します。たとえば、従属関数構成演算子の暗黙の引数を正しく推測することはできません。
(* Only infers (?2 -> ?3) -> (?1 -> ?2) -> (?1 -> ?3) *)
def `.` g f x := g (f x)
この場合、いくつかの追加情報を明示的に提供する必要があります。
(* If we omitted {x}, it would become an implicit argument of `.` *)
def `.` (g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x)
これは次のように拡張できます。
def `.` {A} {B : A -> Type} {C : all {x} -> B x -> Type}
(g : all {x} (y : B x) -> C y) (f : all x -> B x) x := g (f x)
比較のために、同等の Agda 定義を次に示します。
_∘_ : ∀ {A : Set} {B : A → Set} {C : ∀ {x} → B x → Set}
(g : ∀ {x} (y : B x) → C y) (f : ∀ x → B x) x → C (f x)
(g ∘ f) x = g (f x)
注の終わり
上記のメカニズムは実現可能ですか？さらに良いことに、このメカニズムに似たものを実装する言語はありますか?