时间戳

首页 > 解决方案 > 使用接口在 Type 上定义偏函数

typeclass - 使用接口在 Type 上定义偏函数

问题描述

我试图在 Idris 中定义一些东西，这将提供一种以印刷方式表示类型的方法。想一想Show，但Show我不想显示类型的元素，而是显示类型本身。这将具有相同的实际效果，即在Type（给出类型的表示）上定义用户也可以为其类型扩展的部分函数。

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

interface Representable a where
  representation : String

一些可能的实现是

Representable Nat where
  representation = "Nat"

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

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

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

我想出的一个替代方案是创建一个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的表示，而不是它的元素。

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

标签： typeclassidristype-level-computation

解决方案

您可以从 Haskell 中获取想法并使用代理将令牌传递给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})

推荐阅读