1

为了让我的问题有意义，我必须提供一些背景信息。

我认为拥有一种依赖类型的语言来推断一个函数的参数的存在和类型是很有用的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

如果我们做出两个（诚然，毫无根据的）假设：

  1. 必须不存在无法从显式提供的信息中推断出的依赖关系。
  2. 每个自由变量都必须转换为使用defor引入的最后一个标识符的隐式参数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)

显然，两个毫无根据的假设为我们节省了很多打字时间！

注意：当然，这种机制只有在原始假设成立时才有效。例如，我们无法正确推断出依赖函数组合运算符的隐含参数：

(* 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)

笔记结束

上述机制可行吗？更好的是，是否有任何语言可以实现类似这种机制的东西？

4

1 回答 1

1

这听起来像是Coq 中的隐式泛化。

于 2013-01-18T23:13:38.457 回答