Ограничения в экземплярах семейств типов

Я изучаю семейства типов в Haskell, пытаясь определить сложность функций уровня типов, которые я могу определить. Я хочу определить закрытую версию mod на уровне типа, например:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits

type family Mod (m :: Nat) (n :: Nat) :: Nat where
  n <= m => Mod m n = Mod (m - n) n
  Mod m n = m

Однако компилятор (GHC 7.10.2) отвергает это, поскольку ограничение в первом уравнении недопустимо. Как охранники на уровне значения переходят на уровень типа? Возможно ли это в Haskell в настоящее время?


haskell type-families
person prophet-on-that    schedule 31.05.2016    source источник
comment
Возможно, есть функция уровня типа If? Я думаю, что где-то видел, что это использовалось, но я не специалист по библиотекам...   -  person chi    schedule 31.05.2016
comment
Спасибо, вы абсолютно правы, If существует в Data.Type .Бол.   -  person prophet-on-that    schedule 01.06.2016
comment
После этого мне удалось переписать Mod, используя уровень типов If, который успешно скомпилировался. Однако любая попытка уменьшить термин формы Mod m n приводила к исключению переполнения стека. Настройка параметра -freduction-depth показала мне, что GHC уделяет приоритетное внимание расширению m - n части выражения, не понимая, что это никогда не будет возможно. Мне придется изучить расширение DataKinds, чтобы лучше понять его поведение.   -  person prophet-on-that    schedule 01.06.2016
comment
Это очень интересно. Из вашего отчета кажется, что уровень типа If стремится ко всем своим аргументам, что выглядит неправильно.   -  person chi    schedule 01.06.2016

Ответы (1)


arrow_upward
3
arrow_downward

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

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits
import Data.Type.Bool

type family Mod (m :: Nat) (n :: Nat) :: Nat where
  Mod m n = If (n <=? m) (Mod (m - n) n) m

Причина в том, что If само по себе является просто обычным семейством типов, и поведение семейств типов должно начинаться с расширения их аргументов типа (в некотором смысле нетерпеливых) перед использованием аргументов в правой части. Неблагоприятный результат в этом случае заключается в том, что Mod (m - n) n расширяется, даже если n <=? m ложно, следовательно, происходит переполнение стека.

Точно по той же причине логические операторы в Data.Type.Bool не допускайте короткого замыкания. Дано

type family Bottom :: Bool where Bottom = Bottom

Мы видим, что False && Bottom и True || Bottom зависают.

РЕДАКТИРОВАТЬ

На всякий случай, если OP просто заинтересован в семействе типов с требуемым поведением (а не только в более общей проблеме наличия охранников в семействах типов), есть способ выразить Mod таким образом, чтобы завершить :

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}
import GHC.TypeLits

type Mod m n = Mod1 m n 0 m

type family Mod1 (m :: Nat) (n :: Nat) (c :: Nat) (acc :: Nat) :: Nat where
  Mod1 m n n acc = Mod1 m n 0 m
  Mod1 0 n c acc = acc
  Mod1 m n c acc = Mod1 (m - 1) n (c + 1) acc
person Alec    schedule 28.07.2016