Как я могу ссылаться на метод интерфейса Idris из той же декларации интерфейса? - PullRequest
Новая
       11

Как я могу ссылаться на метод интерфейса Idris из той же декларации интерфейса?

0 голосов
/ 24 декабря 2018

Я создал небольшой класс TotalOrder, который обладает более сильными свойствами доказательства, чем обычный класс Ord.Проблема в том, что эти свойства должны ссылаться друг на друга так, как я не знаю, как это сделать, синтаксически.

Мне нужно ссылаться на мой тип lessThan в других методах интерфейса, но этопохоже, что его обрабатывают как обычную (неявно forall'd) переменную. 

module Order

%default total

public export
data Ordering : (t -> t -> Type) -> t -> t -> Type where
  LessThan : f x y -> Ordering f x y
  Equal : x = y -> Ordering f x y
  GreaterThan : f y x -> Ordering f x y

public export
interface TotalOrder a where
  lessThan : a -> a -> Type
  compare : (x, y : a) -> Ordering lessThan x y
  ltNeq : lessThan x y -> x = y -> Void
  ltNgt : lessThan x y -> lessThan y x -> Void

-- Implementation for Nats

compareNat : (x, y : Nat) -> Ordering LT x y
compareNat x y = ...

ltNeqNat : LT x y -> x = y -> Void
ltNeqNat lt eq = ... 

ltNgtNat : LT x y -> LT y x -> Void
ltNgtNat lt gt = ...

implementation TotalOrder Nat where
  lessThan = LT
  compare = compareNat -- THIS LINE REFUSES TO COMPILE
  ltNeq = ltNeqNat
  ltNgt = ltNgtNat

Насколько я могу определить, проверка типов автоматически предполагает, что lessThan s в положении функции в ltNeq и ltNgt совпадают с lessThan, объявленным в интерфейсе, но lessThan в позиции аргумента в compare рассматривается как обычный аргумент для compare, что означает, что тип для реализации Nat равен

compare : {lessThan : Nat -> Nat -> Type} -> (x, y : Nat) -> Ordering lessThan x y

вместо

compare : (x, y : Nat) -> Ordering LT x y

и compare = compareNat больше не проверяет тип.Когда я сталкиваюсь с этой проблемой в функциях верхнего уровня, полная квалификация имени работает, но я не уверен, каким будет полное имя здесь, и очевидные идеи (Order.lessThan, TotalOrder.lessThan, Order.TotalOrder.lessThan) все получают "нет такой переменной" d.

...