Idris：是否可以通过接口限制功能输出？

Question

我正在尝试为可以（在某种意义上，与问题无关）转换为其他值的值创建一个接口。目前定义如下：

interface Convertible c where
    target : c -> Type
    convert: (item: c) -> (target item)

因此，在实现此接口时，必须同时提供转换和目标类型，这可能取决于要转换的值。

在现实生活中，每个转换目标自然也可以转换 - 例如：

implementation Convertible () where
    -- This is allowed, since we're implementing Convertible for unit type right now.
    target _ = ()
    convert _ = ()

implementation Convertible String where
    -- This is allowed, since Convertible is already implemented for unit type.
    target _ = ()
    convert _ = ()

implementation Convertible Double where
    -- This doesn't make sense, since Integer isn't Convertible.
    target _ = Integer
    convert item = cast $ floor item

此外，任何可转换的值都可以“包装”到提供的类型中，这也将是可转换的。但是，如果转换目标本身可能无法转换，则会导致以下问题：

data Wrapper : Type -> Type where
    -- The type should be restricted here, otherwise we'll have signature clashes
    -- fromInteger here is only as an example, but the real-life case is similar
    fromInteger : (Convertible c) => c -> Wrapper c
    -- This works, but is extremely unergonomic, so I'd like to avoid it:
    -- fromInteger : c -> Wrapper c

-- ...but with the restriction on data type, we can't implement this:
implementation (Convertible c) => Convertible (Wrapper c) where
    target (fromInteger inner) = Wrapper (target inner)
    convert (fromInteger inner) = fromInteger (convert inner)

错误：

test.idr:32:35-61:
   |
32 |     convert (fromInteger inner) = fromInteger (convert inner)
   |                                   ~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.Main.Wrapper c implementation of Main.Convertible, method convert with expected type
        Main.Wrapper c implementation of Main.Convertible, method target c constraint (fromInteger inner)

Can't find implementation for Convertible (target inner)

那么，是否可以让 Idris 理解（并检查）只要 c 是 Convertible，target c 总是 Convertible？

Answer 1

可能可以使用 auto 和 %hint 来减少样板文件。

interface Convertible c where
    target : c -> Type
    p : (item : c) -> Convertible (target item)
    convert: (item: c) -> target item

implementation Convertible () where
    -- This is allowed, since we're implementing Convertible for unit type right now.
    target _ = ()
    convert _ = ()
    p _ = %implementation

implementation Convertible String where
    -- This is allowed, since Convertible is already implemented for unit type.
    target _ = ()
    convert _ = ()
    p _ = %implementation


data Wrapper : Type -> Type where
    -- The type should be restricted here, otherwise we'll have signature clashes
    -- fromInteger here is only as an example, but the real-life case is similar
    fromInteger : (Convertible c) => c -> Wrapper c
    -- This works, but is extremely unergonomic, so I'd like to avoid it:
    -- fromInteger : c -> Wrapper c

-- ...but with the restriction on data type, we can't implement this:
implementation (Convertible c) => Convertible (Wrapper c) where
    target (fromInteger inner) = Wrapper (target inner)
    convert (fromInteger inner) = let _ = p inner in fromInteger (convert inner)
    p (fromInteger inner) = let _ = p inner in %implementation

implementation Convertible Double where
    -- This doesn't make sense, since Integer isn't Convertible.
    target _ = Integer
    convert item = cast $ floor item
    p _ = %implementation

失败 Can't find implementation for Convertible Integer

Idris：是否可以通过接口限制功能输出？

Idris: is it possible to restrict function output by interface?

dependent-type

associated-types

idris