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

问题描述

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

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)

因此，只要target c是Convertible，是否有可能使Idris理解（并检查）c始终是Convertible？

解决方法

也许可以使用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