Ограничения типа в Dafny: реализация Show для бинарного типа отношения

Я определил тип полиморфного бинарного отношения (класс) в Dafny:

class binRel<S,T>

Фактическая декларация:

class binRel<S(!new,==),T(!new,==)>.

Я хотел бы добавить новое ограничение типа: типы S и T должны реализовывать операцию "show" (возвращая строку).

Мое чтение Справочного руководства Dafny показывает, что Dafny поддерживает только несколько встроенных ограничений типа: == и, очевидно, !new, и что нет никакого способа потребовать поддержки этого типа, например, какой-то конкретной черты.

Возможно, я ошибаюсь и что обновления более свежие, чем справочник, предоставили такие возможности. Мне повезло? Если нет, возможно, есть обходной путь?


dafny
person Kevin S    schedule 05.03.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Правильно, в Dafny всего несколько встроенных ограничений типов. Не существует механизма, требующего, чтобы тип расширял признак.

Я не знаю хорошего обходного пути для объектно-ориентированного/императивного фрагмента Дафни. В чистом фрагменте вы можете обойти это, используя первоклассные функции.

datatype MyPair<A,B> = MakePair(a: A, b: B)

type Show<!A> = A -> string

function ShowMyPair<A,B>(sa: Show<A>, sb: Show<B>): Show<MyPair<A,B>>
{
  (p: MyPair<A,B>) => "(" + sa(p.a) + "," + sb(p.b) + ")"
}
person James Wilcox    schedule 05.03.2018