Могу ли я написать универсальную функцию-оболочку для интерфейса Wrapper, представляющего тип, который является оболочкой для какого-то другого типа?

Полный пример кода ниже (который успешно компилируется) является упрощенным и слегка надуманным примером моей проблемы.

NatPair - это пара Nat, и я хочу «поднять» бинарныеNum операции до NatPair точечно, используя функцию lift_binary_op_to_pair.

Но я не могу реализовать Num NatPair, потому что NatPair не является конструктором данных.

Итак, я заключаю его в тип WrappedNatPair и могу предоставить Num реализацию для этого типа с соответствующими «приподнятыми» версиями + и *.

Затем я хочу обобщить идею типа оболочки с помощью моего Wrapper интерфейса.

Функция lift_natpair_bin_op_to_wrapped может поднять двоичную операцию с NatPair до WrappedNatPair, а код реализации полностью основан на методах интерфейса unwrap и wrap Wrapper.

Но если я попытаюсь обобщить

lift_bin_op_to_wrapped : Wrapper t => BinaryOp WrappedType -> BinaryOp t

тогда подпись типа даже не скомпилируется с ошибкой:

 `-- Wrapping.idr line 72 col 23:
     When checking type of Main.lift_bin_op_to_wrapped:
     Can't find implementation for Wrapper t

(где место ошибки - это место ":" в сигнатуре типа).

Я думаю, проблема в том, что t нигде не фигурирует в сигнатуре типа для метода Wrapper interface WrapperType, поэтому WrapperType нельзя вызывать где-либо, кроме как внутри самого определения интерфейса.

(Обходной путь состоит в том, чтобы каждый раз писать стандартные lift_<wrapped>_bin_op_to_<wrapper> методы с одним и тем же кодом реализации op x y = wrap $ op (unwrap x) (unwrap y), что недопустимо. Но я хотел бы иметь четкое представление о том, почему я не могу написать общий lift_bin_op_to_wrapped метод.)

Полный код, который успешно компилируется:

%default total

PairedType : (t : Type) -> Type
PairedType t = (t, t)

NatPair : Type
NatPair = PairedType Nat

data WrappedNatPair : Type where
  MkWrappedNatPair : NatPair -> WrappedNatPair

equal_pair : t -> PairedType t
equal_pair x = (x, x)

BinaryOp : Type -> Type
BinaryOp t = t -> t -> t

lift_binary_op_to_pair : BinaryOp t -> BinaryOp (PairedType t)
lift_binary_op_to_pair op (x1, x2) (y1, y2) = (op x1 y1, op x2 y2)

interface Wrapper t where
  WrappedType : Type
  wrap : WrappedType -> t
  unwrap : t -> WrappedType

Wrapper WrappedNatPair where
  WrappedType = NatPair
  wrap x = MkWrappedNatPair x
  unwrap (MkWrappedNatPair x) = x

lift_natpair_bin_op_to_wrapped : BinaryOp NatPair -> BinaryOp WrappedNatPair
lift_natpair_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y)

Num WrappedNatPair where
  (+) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (+))
  (*) = lift_natpair_bin_op_to_wrapped (lift_binary_op_to_pair (*))
  fromInteger x = wrap $ equal_pair (fromInteger x)

WrappedNatPair_example : the WrappedNatPair 8 = (the WrappedNatPair 2) + (the WrappedNatPair 6)
WrappedNatPair_example = Refl

(Платформа: Ubuntu 16.04 с Idris 1.1.1-git: 83b1bed.)


wrapper dependent-type idris
person Philip Dorrell    schedule 12.08.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я думаю, проблема в том, что t нигде не появляется в сигнатуре типа для метода WrapperType интерфейса Wrapper, поэтому WrapperType не может быть вызван нигде, кроме как внутри самого определения интерфейса.

Ты прямо здесь. Вот почему вы получаете эту ошибку. Вы можете исправить эту ошибку компиляции, явно указав, какие типы являются оболочкой следующим образом:

lift_bin_op_to_wrapped : Wrapper w => BinaryOp (WrappedType {t=w}) -> BinaryOp w
lift_bin_op_to_wrapped {w} op x y = ?hole

Но это, вероятно, вам не поможет, потому что Идрис каким-то образом не может установить соответствие между w и WrappedType. Мне бы очень хотелось увидеть объяснение этому факту. В основном компилятор (я использую Idris 1.0) говорит мне следующее:

- + Wrap.hole [P]
 `--           w : Type
               x : w
               y : w
      constraint : Wrapper w
              op : BinaryOp WrappedType
     -----------------------------------
      Wrap.hole : w

Ваш WrappedType метод интерфейса с зависимым типом несколько хитроумно реализует сопоставление с образцом для типов. Думаю, это может быть причиной проблем. Если вы знакомы с Haskell, вы можете увидеть некоторое сходство между вашими WrappedType и -XTypeFamilies. См. Этот вопрос: Сопоставление шаблонов с типом в Idris

Хотя вы все еще можете реализовать общую функцию оболочки. Вам только нужно по-другому оформить интерфейс. Я использую трюк, описанный в этом вопросе: Ограничение аргумента функции в интерфейсе < / а>

interface Wraps (from : Type) (to : Type) | to where
  wrap   : from -> to
  unwrap : to   -> from

Wraps NatPair WrappedNatPair where
   wrap = MkWrappedNatPair
   unwrap (MkWrappedNatPair x) = x

lift_bin_op_to_wrapped : Wraps from to  => BinaryOp from -> BinaryOp to
lift_bin_op_to_wrapped op x y = wrap $ op (unwrap x) (unwrap y)

Num WrappedNatPair where
  (+) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat} (+))
  (*) = lift_bin_op_to_wrapped (lift_binary_op_to_pair {t=Nat}(*))
  fromInteger = wrap . equal_pair {t=Nat} . fromInteger

Это компилируется и отлично работает.

person Shersh    schedule 12.08.2017