使用接口在 Type 上定义偏函数答案

【问题标题】：Using interfaces to define partial functions on Type使用接口在 Type 上定义偏函数
【发布时间】：2019-07-03 23:11:51
【问题描述】：

我正在尝试在 Idris 中定义 something，这将提供一种以印刷方式表示类型的方法。想想Show，但不是Showing 类型的元素，我想显示类型本身。这与在 Type 上定义一个部分函数（提供类型的表示）具有相同的实际效果，用户也可以针对他们的类型进行扩展。

鉴于“用户可以扩展功能”的要求，我的第一个想法是使用接口。所以看起来像这样：

interface Representable a where
  representation : String

一些可能的实现是

Representable Nat where
  representation = "Nat"

但是，我遇到了一个问题。假设我想定义函数类型的表示。那将是其域的表示、箭头和其范围的表示。所以像

(Representable a, Representable b) => Representable (a -> b) where
  representation = representation ++ " -> " ++ representation

问题现在很明显了。编译器无法推断右侧的representation 的类型。

我想出的另一种选择是创建一个带有“人工”参数的Representation 类型：

data Representation : Type -> Type where
  Repr : (a : Type) -> String -> Representation a

这会导致

interface Representable a where
  representation : Representation a

然后

Representable Nat where
  representation = Repr Nat "Nat"

(Representable d, Representable r) => Representable (d -> r) where
  representation = Repr (d -> r) $
    (the (Representation d) representation)
    ++ " -> "
    ++ (the (Representation r) representation)

但是，当然，我得到了错误

Representations.idr:13:20-127:
   |
13 |   representation = Repr (d -> r) $ (the (Representation d) representation) ++ " -> " ++ (the (Representation r) representation)
   |                    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Representations.Representations.d -> r implementation of Representations.Representable, method representation with expected type
        Representation (d -> r)

When checking argument a to constructor Representations.Repr:
        No such variable d

但是，我希望 representation 没有参数——显然，因为它是 type 的表示，而不是它的元素。

是否有人对如何解决这个特定错误有任何建议，或者更好的是，如何以某种不那么可怕的方式实现我的想法？

【问题讨论】：

标签： typeclass idris type-level-computation

【解决方案1】：

您可以从 Haskell 中获取一个想法并使用 proxy 将令牌传递给 representation，而无需任何术语级内容：

data Proxy a = MkProxy

interface Representable a where
  representation : Proxy a -> String

Representable Nat where
  representation _ = "Nat"

(Representable a, Representable b) => Representable (a -> b) where
  representation {a = a} {b = b} _ = representation (MkProxy {a = a}) ++ " -> " ++ representation (MkProxy {a = b})

【讨论】：