Idris:是否可以通过接口限制功能输出?

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

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

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 理解(并检查)只要 cConvertibletarget 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