Как работает `HFix` в пакете multirec на Haskell? - PullRequest
Новая
       24

Как работает `HFix` в пакете multirec на Haskell?

5 голосов
/ 15 марта 2012

Я понимаю обычный комбинатор с фиксированной точкой и думаю, что понимаю комбинаторы с фиксированным n-го рода высшего порядка, но HFix ускользает от меня Не могли бы вы привести пример набора типов данных и их (полученных вручную) фиксированных точек, к которым можно применить HFix к.

1 Ответ

5 голосов
/ 16 марта 2012

Естественным эталоном является статья Универсальное программирование с фиксированными точками для взаимно рекурсивных типов данных , где объясняется multirec пакет .

HFix - тип с фиксированной точкойкомбинатор для взаимно рекурсивных типов данных.Это хорошо объяснено в разделе 3.2 в статье, но идея состоит в том, чтобы обобщить этот шаблон: 

 Fix :: (∗ -> ∗) -> ∗
 Fix2 :: (∗ -> ∗ -> ∗) -> (∗ -> ∗ -> ∗) -> ∗

до 

 Fixn :: ((∗ ->)^n * ->)^n ∗
 ≈
 Fixn :: (*^n -> *)^n -> *

Чтобы ограничить, сколько типов он делает фиксированной точкойони используют конструкторы типов вместо * ^ n.Они дают пример типа данных AST, взаимно рекурсивный по трем типам в статье.Вместо этого я предлагаю вам, пожалуй, самый простой пример.Давайте исправим этот тип данных: 

data Even = Zero | ESucc Odd deriving (Show,Eq)
data Odd  = OSucc Even       deriving (Show,Eq)

Давайте введем семейный GADT для этого типа данных, как это сделано в разделе 4.1 

data EO :: * -> * where
  E :: EO Even
  O :: EO Odd

EO Even будет означать, что мы несемвокруг четного числа.Нам нужны экземпляры El для этого, чтобы указать, какой конкретный конструктор мы ссылаемся при написании EO Even и EO Odd соответственно. 

instance El EO Even where proof = E
instance El EO Odd  where proof = O

Они используются как ограничения для HFunctor instance для I .

Давайте теперь определим функтор шаблона для четного и нечетного типа данных.Мы используем комбинаторы из библиотеки.Конструктор типа :>: помечает значение своим индексом типа: 

type PFEO = U      :>: Even   -- ≈ Zero  :: ()      -> EO Even
        :+: I Odd  :>: Even   -- ≈ ESucc :: EO Odd  -> EO Even
        :+: I Even :>: Odd    -- ≈ OSucc :: EO Even -> EO Odd

Теперь мы можем использовать HFix, чтобы связать узел вокруг этого функтора шаблона: 

type Even' = HFix PFEO Even
type Odd'  = HFix PFEO Odd

Теперь они изоморфны EO Even и EO Odd, и мы можем использовать функции hfrom и hto , если мы сделаем его экземпляром Fam: 

type instance PF EO = PFEO

instance Fam EO where
  from E Zero      = L    (Tag U)
  from E (ESucc o) = R (L (Tag (I (I0 o))))
  from O (OSucc e) = R (R (Tag (I (I0 e))))
  to   E (L    (Tag U))           = Zero
  to   E (R (L (Tag (I (I0 o))))) = ESucc o
  to   O (R (R (Tag (I (I0 e))))) = OSucc e

Простой маленький тест: 

test :: Even'
test = hfrom E (ESucc (OSucc Zero))

test' :: Even
test' = hto E test

*HFix> test'
ESucc (OSucc Zero)

Еще один глупый тест с алгеброй, поворачивающей Even и Odd с к их Int значению: 

newtype Const a b = Const { unConst :: a }

valueAlg :: Algebra EO (Const Int)
valueAlg _ = tag (\U             -> Const 0)
           & tag (\(I (Const x)) -> Const (succ x))
           & tag (\(I (Const x)) -> Const (succ x))

value :: Even -> Int
value = unConst . fold valueAlg E
...