haskell - 关注点分离 : when is it best to disassociate semantics from syntax?

Question

选择

类型类非常出色，因为它们允许我们将额外的结构连接到现有类型。从而使我们能够推迟一些设计决策，而不是在构思时匆忙做出决定。

另一方面，例如，在面向对象编程中，我们被迫考虑类型需要立即执行什么操作，以及稍后出现的或需要的任何附加结构将被合并到子类型中。

万事皆有其目的。我想知道在 Agda 的背景下什么时候最好选择其中之一。

非人为示例

将以下内容用于 n -ary 函数 s → s → ... → s → t，

Func : ∀ {ℓ} (a : ℕ) (s : Set ℓ) (t : Set ℓ) → Set ℓ
Func zero s t = t
Func (suc a) s t = s → Func a s t

在定义编程语言的语法时，我们可能会将类型符号视为一个命名项，该命名项是通过采用许多其他此类命名项而“形成”的，并且它的含义是可以理解的通过采用上述参数并生成具体 Agda Set 的操作。

record Type₁ : Set₁ where
 constructor cons₁
 field
  name₁      : String
  arity₁     : ℕ
  paramters₁ : Vec Type₁ arity₁
  semantics₁ : Func arity₁ Type₁ Set

open Type₁

因此我们将符号和解释打包为一种类型。或者，我们可以将两者分开:

record Type₂ : Set₁ where 
 constructor cons₂
 field
  name₂      : String
  arity₂     : ℕ
  paramters  : Vec Type₂ arity₂

open Type₂ {{...}}

record HasMeaning (t : Type₂) : Set₁ where
  field
    semantics₂ : Func (arity₂ {{t}}) Type₂ Set

open HasMeaning {{...}}

( 请注意，由于使用 Func，我们需要 Type2 存在于 Set₁ 中，尽管它确实存在于 Set 中 上面的 HasMeaning 中。)

哪个最好，为什么？特别是从编程的角度来看哪个更好，从证明的角度来看哪个更好？

语义

假设我们实际上想用我们的类型(符号)做一些事情，例如将它们解释为实际的 Agda 类型，那么我们可以使用第一个定义轻松做到这一点:

⟦_⟧₁ : Type₁ → Set 
⟦ cons₁ name₁ 0 [] semantics₁ ⟧₁ = semantics₁
⟦ cons₁ name₁ (suc n) (hd ∷ tl) semantics₁ ⟧₁ = 
     ⟦ cons₁ name₁ n tl (semantics₁ hd) ⟧₁

没什么聪明的。如果没有“参数”，那么语义函数必然是一个 Agda Set，我们就完成了；否则，我们将第一个类型参数提供给语义函数并递归以获得具体的Set。

第二个定义有点烦人，因为每次我们想要使用类型的语义时都需要放置类型类约束，这对我来说太多了!

⟦_⟧₂ : (t : Type₂) {{_ : HasMeaning t}} → Set
⟦ cons₂ name₂ 0 [] ⟧₂ {{s}} = semantics₂ {{s}}
⟦ cons₂ name₂ (suc n) (hd ∷ tl) ⟧₂ {{s}} = 
     ⟦ cons₂ name₂ n tl ⟧₂ 
     {{ record { semantics₂ = semantics₂ {{s}} hd } }}

更糟糕的是，如果我们有冲突的语义实例怎么办？也许我们最多只需要一个实例，我们如何实现这一目标？

所以，就我的目的而言，似乎第一个是最好的......或者不是......

平等

第二个定义明确承认可判定的相等性，因为自然数和字符串具有可判定的相等性。然而，第一个原因并不在于解释功能。当两个类型(符号)具有相同的名称、属性和参数时，可以通过说它们完全相同来回避这个问题；无论解释如何:

postulate eq₁-desire : ∀ {n a p S T} → cons₁ n a p S ≡ cons₁ n a p T

遗憾的是，这并没有给我们提供计算，这可以通过使用 trustMe 来修复。 .

决定

据我所知，从上面的漫谈来看，第一种方法和 trustMe 是可行的方法。但是，我不太习惯使用 trustMe ---我对此知之甚少。

任何关于走哪条路的建议，或者任何关于采取哪种方法的理由，我们将不胜感激。谢谢!

Answer 1

我认为，首先您应该将名称-数量-语义部分与类型分开。由于每个 Type 都可以强制转换为 Set，因此您可以将语义表示为从 Set 到 Set 的函数而不是从 Type 到 Set (与您的 Type₁ 不同，这也是严格正数)。其外观如下:

record Atom : Set₁ where
  constructor packAtom
  field
    name      : String
    arity     : ℕ
    semantics : Func arity Set Set

record Type : Set₁ where
  inductive
  constructor packType
  field atom : Atom

  open Atom atom

  field parameters : Vec Type arity

mutual
  ⟦_⟧ : Type -> Set
  ⟦ packType (packAtom n ar sem) ts ⟧ = ⟦ ts ⟧s sem

  ⟦_⟧s : ∀ {ar} -> Vec Type ar -> Func ar Set Set -> Set
  ⟦ []     ⟧s A = A
  ⟦ t ∷ ts ⟧s F = ⟦ ts ⟧s (F ⟦ t ⟧) 

那么你的问题可以重述为“有没有办法强制数量和语义由名称确定？”。但 Agda 并不强制实例的全局唯一性。此外，您似乎想要内化一个元定理“每个名称都有一个唯一的语义”，因此您可以在代码中使用它，但那就是想要的太多了。您能举例说明为什么需要这样做吗？