在 Idris 中，“Eq a"是一种类型，我可以为它提供一个值吗? [英] In Idris, is "Eq a" a type, and can I supply a value for it?

问题描述

在下面，example1 是标准语法(如文档所示)，Eq a 作为约束.在example2中，我直接指定Eq a作为参数的类型，编译器接受.但是，尚不清楚我可以指定什么作为该类型的值.对于特定类型 a，例如 Nat，我认为以某种方式指定 Eq Nat 的实现是有意义的，要么是默认实现，或其他一些命名实现.

In the following, example1 is standard syntax (as documented), with Eq a as a constraint. In example2, I specify Eq a directly as the type of a parameter, and the compiler accepts it. However it is unclear what I can specify as a value of that type. For a specific type a, eg Nat, I assume it would make sense to somehow specify an implementation of Eq Nat, either the default implementation, or some other named implementation.

%default total

example1: Eq a => (x : a) -> (y : a) -> Type
example1 {a} x y = ?example1_rhs

example1b: Eq a => (x : a) -> (y : a) -> Type
example1b {a} x y = x == y = True

example2: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type
example2 a eqa x y = ?example2_rhs

example2b: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type
example2b a eqa x y = x == y = True

eq_nat : Eq Nat
eq_nat = ?eq_nat_rhs

example_of_example2 : Type
example_of_example2 = example2 Nat eq_nat 3 3

产生的漏洞:

- + Main.example1_rhs [P]
 `--                  a : Type
                      x : a
                      y : a
             constraint : Eq a
     --------------------------
      Main.example1_rhs : Type

- + Main.example2_rhs [P]
 `--                  a : Type
                    eqa : Eq a
                      x : a
                      y : a
     --------------------------
      Main.example2_rhs : Type

- + Main.eq_nat_rhs [P]
 `-- Eq Nat

据我所知，我实际上不能将 example2b 用作函数，除非我有办法为 Eq a.

As far as I can tell, I can't actually use example2b as a function unless I have some way to specify a value for the second parameter of type Eq a.

在某些情况下，能够将接口约束应用于参数的值(而不是参数的类型)真的很有用，所以我希望这是 Idris 的有效功能.

There are situations where it would be genuinely useful to be able to apply an interface constraint to the value of a parameter (as opposed to the type of a parameter), so I'm hoping that this is a valid feature of Idris.

推荐答案

您可以使用命名实现:

[eq_nat] Eq Nat where { ... }
...
example_of_example2 : Type
example_of_example2 = example2 Nat eq_nat 3 3

命名实现的一个有用的应用是定义 Monoid 的多个实现:

A useful application of named implementations are defining multiple implementation of Monoid:

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

[PlusNatMonoid] Monoid Nat using PlusNatSemi where
  neutral = 0

[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1

<小时>

评论:获取默认实例

---

To comment : To get the default instance

getEq : (a : Type) -> {auto inst : Eq a} -> Eq a
getEq a {inst} = inst

然后你可以拥有你的默认实例:

Then you can have your default instance:

getEq (List Nat) -- => implementation of Eq...

这篇关于在 Idris 中，“Eq a"是一种类型，我可以为它提供一个值吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！