Как я могу создать функцию для приведения значений: x `as` T = y? - PullRequest
Новая
       15

Как я могу создать функцию для приведения значений: x `as` T = y?

1 голос
/ 07 февраля 2020

У меня есть интерфейс для преобразования вещей одного типа this в другой тип target. 

interface ConvertibleTo (target : Type) (this : Type) where
    convert : this -> target

Можно ли как-то написать функцию, которая принимает некоторое значение this, затем target type, а затем выдает значение target type?

Я пытался написать это 

-- Example: 1 `as` String = "1"
as : ConvertibleTo target this => this -> (target : Type) -> target
as value _ = convert value

, но оно не работает. Компилятор говорит: 

   |
27 | as value _ = convert value
   |              ~~~~~~~~~~~~~

When checking right hand side of as with expected type
    iType

Can't find implementation for ConvertibleTo iType this

И я не понимаю это сообщение, потому что я уже добавил ограничение.

1 Ответ

1 голос
/ 08 февраля 2020

Проблема в том, что с (target : Type) вы вводите новую переменную, внутренне называемую iType (так как target уже назначено в другом месте), к которой относится -> target. Поскольку ограничение использует target, оно должно следовать после этого аргумента. Ограничения - это просто волшебные неявные аргументы c, поэтому вам не нужно указывать их сначала: 

interface ConvertibleTo (target : Type) (this : Type) where
    convert : this -> target

as : this -> (target : Type) -> ConvertibleTo target this => target
as x _ = convert x

ConvertibleTo String Nat where
    convert = show

> as (S Z) String
"1"

(Если вы не знали, в стандарте уже есть интерфейс ConvertibleTo) библиотека с некоторыми полезными реализациями: Cast from to)

...