对类型构造函数参数具有接口(interface)约束的 Idris 相关记录

Question

是否可以对 idris 中依赖记录的类型构造函数的参数进行接口(interface)约束？
假设我有一个接口(interface)Show : Type -> Type .现在我需要对以下依赖记录进行约束:

record Source s where
   constructor MkSource
   initial : s

我需要对参数 s 施加约束所以它应该始终是 Show 的一个实例.如何做到这一点？

Answer 1

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

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