Ограничение типа записи в Идрисе

Я пытаюсь написать запись в Идрисе, но у нее есть общий параметр, который должен быть ограничен интерфейсом. Для обычных типов объединения я могу написать:

data BSTree : (a : Type) -> Type where
  Empty : Ord a => BSTree a
  Node  : Ord a => BSTree a -> a -> BSTree a

но я пытаюсь выяснить синтаксис для того же самого, только с записью. Я пробовал что-то вроде:

record Point a where
  constructor MkPoint : Eq a => a -> a -> Point a
  x : a
  y : a

но он не компилируется.

Есть ли способ сделать это в Идрисе?

TIA


record typeclass idris
person Rouan van Dalen    schedule 17.07.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Сделать это можно так:

record Point a where
  constructor MkPoint
  x : Eq a => a
  y : Eq a => a

Хотя на самом деле вам не следует этого делать. Вместо этого лучше использовать какой-нибудь умный конструктор, какую-нибудь другую функцию, например mkPoint : Eq a => a -> a -> MkPoint a. В реальной жизни вам не нужно ограничивать типы полей для типа данных. Прочтите о -XDataTypeContexts расширении Haskell.

person Shersh    schedule 17.07.2017
comment
Спасибо. Я знаю, что вам не следует добавлять ограничения непосредственно в поля. Вот почему в моем примере записи я попытался добавить ограничение в конструктор данных MkPoint (что я также делаю для типа объединения). Могу ли я наложить ограничение на конструктор данных MkPoint? - person Rouan van Dalen; 18.07.2017
comment
@RouanvanDalen Нет, нет возможности добавлять ограничения непосредственно в конструктор. И в этом нет реального смысла, потому что нет семантической разницы между наличием ограничений для полей и наличием ограничений для constructor. Только синтаксическая разница. - person Shersh; 18.07.2017