模仿Agda中的类型的Haskell规范(仅限一个实例)

Question

Agda的记录和instance关键字的混合使我们的行为类似于Haskell的类型类.而且,忽略instance关键字,我们可以为同一类型设置多个实例 - 这是我们在Haskell中无法做到的.

我正处于需要Haskell的单实例要求的地步,但在Agda中.是否有编译器选项或一些技巧/启发式来强制执行此操作？

现在我采取的方法是,

record Yo (n : ?) : Set where
  field
    sem : (some interesting property involving n)

open Yo {{...}}

postulate UniqueYo: ? {n} (p q : Yo n) ? p ? q

然而,每当我实际使用UniqueYo缺乏计算时,我的目标就会充斥着...| UniqueYo p p我喜欢的地方...| refl或完全重写为正常形式的东西.

任何帮助表示赞赏!

Answer 1

使用较新版本的 Agda，您可以使用PropUniverse来获取类型的定义唯一性：

\n

{-# OPTIONS --prop #-}\nmodule UniquenessUsingProp where\nopen import Data.Nat.Base\nopen import Relation.Binary.PropositionalEquality\n\n-- Convert a Set to a Prop. This could be avoided if e.g.\n-- we defined > as a Prop (like in the example in the docs\n-- linked above)\ndata Squash {\xe2\x84\x93} (A : Set \xe2\x84\x93) : Prop \xe2\x84\x93 where\n  squash : A \xe2\x86\x92 Squash A\n\n-- record Yo (n : \xe2\x84\x95) : Prop where -- Both variants works\nrecord Yo (n : \xe2\x84\x95) : Set where\n  field\n    sem : Squash (n + 1 > n * 2)\n\n-- Since `Yo n` is a Prop and not a set, it can\'t be the\n-- direct argument of \xe2\x89\xa1. This is not a problem since \n-- it\'s definitionally equal anyways.\nUniqueYo : \xe2\x88\x80 {n} (P : Yo n \xe2\x86\x92 Set) (p q : Yo n) \xe2\x86\x92 P p \xe2\x89\xa1 P q\nUniqueYo P p q = refl\n

\n

产生类似结果的另一种选择是使用证明不相关的记录字段：

\n

module UniqunessUsingProofIrrelevance where\nopen import Data.Nat.Base\nopen import Relation.Binary.PropositionalEquality\n\nrecord Yo (n : \xe2\x84\x95) : Set where\n  field\n    .sem : n + 1 > n * 2\n\nopen Yo {{...}}\n\nUniqueYo : \xe2\x88\x80 {n} (p q : Yo n) \xe2\x86\x92 p \xe2\x89\xa1 q\nUniqueYo p q = refl\n

\n

在这两种情况下，实际使用 Yo 中的值可能很困难，因为您需要让 Agda 相信您的代码不依赖于 中的具体值sem，例如，仅在其上使用荒谬的模式匹配，或者Prop分别生成 或 中的值，提供它作为不相关函数的参数。

\n