Idris 依赖记录，对类型构造函数参数具有接口约束

Question

是否可以对 idris 中依赖记录的类型构造函数的参数进行接口约束？ 假设我有一个界面

Show : Type -> Type

。现在我需要对以下依赖记录施加约束：

record Source s where
   constructor MkSource
   initial : s

我需要对参数

s

施加约束，使其始终是

Show

的实例。如何实现这一目标？

Answer 1

Idris 正在大力开发，但根据最近发给 idris 组的电子邮件，记录语法当前不支持带有接口的约束类型：

https://groups.google.com/forum/#!topic/idris-lang/HMeTylslyFc

您将需要使用数据类型语法，例如

module Main

data Source: Type -> Type where
    MkSource: Show s => s -> Source s


x: Source Int
x = MkSource 3

showSource: Source s -> String
showSource  (MkSource x) = show $ x

testMe: (showSource $ Main.x = "3")
testMe = Refl

Answer 2

你可以这样做：

record a {auto eq : Eq a} where
  constructor MkThing
  target : Int
  value : a 

来源：Discord