Использование интерфейсов для определения частичных функций на типе - PullRequest
Новая
       54

Использование интерфейсов для определения частичных функций на типе

2 голосов
/ 04 июля 2019

Я пытаюсь определить что-то в 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 с правой стороны.

Одна альтернатива, которую я предложил, - создать тип 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 был без аргументов - очевидно, так как это представление типа , а не его элементов.

Есть ли у кого-нибудь предложение о том, как это исправитьконкретная ошибка, или еще лучше, как реализовать мою идею не таким уж ужасающим способом?

1 Ответ

3 голосов
/ 05 июля 2019

Вы можете взять идею из 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})
...