Как заставить катаморфизмы работать с параметризованными / индексированными типами?

Question

Недавно я немного узнал о F-алгебрах: https://www.fpcomplete.com/user/bartosz/understanding-algebras. Я хотел поднять эту функциональность до более продвинутых типов (индексированных и более привязанных). Кроме того, я проверил "Предоставление Haskell продвижения" ( http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf), что было очень полезно, потому что оно давало названия моим собственным расплывчатым "изобретения".

Тем не менее, я не могу создать единый подход, который работает для всех форм.

Алгебрам нужен некоторый "тип носителя", но структура, которую мы пересекаем, ожидает определенной формы (сама применяется рекурсивно), поэтому я придумал контейнер "Dummy", который может нести любой тип, но имеет такую ​​форму, как ожидалось. Затем я использую семейство типов, чтобы соединить их.

Этот подход, кажется, работает, приводя к довольно общей сигнатуре для моей функции 'cata'.

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

Так как IFunctor1 и IFunctor2 не имеют дополнительных переменных, я попытался объединить их, добавив (через семейство типов) к типу функции сохранения индекса, но это, похоже, недопустимо из-за экзистенциального количественного определения, поэтому у меня осталось несколько версий тоже.

Есть ли способ объединить эти 2 случая? Я пропустил некоторые трюки, или пока это просто ограничение? Есть ли другие вещи, которые можно упростить?

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE Rank2Types                #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}
module Cata where

-- 'Fix' for indexed types (1 index)
newtype Mu1 f a = Roll1 { unRoll1 :: f (Mu1 f) a }
deriving instance Show (f (Mu1 f) a) => Show (Mu1 f a)

-- 'Fix' for indexed types (2 index)
newtype Mu2 f a b = Roll2 { unRoll2 :: f (Mu2 f) a b }
deriving instance Show (f (Mu2 f) a b) => Show (Mu2 f a b)

-- index-preserving function (1 index)
type s :-> t = forall i. s i -> t i

-- index-preserving function (2 index)
type s :--> t = forall i j. s i j -> t i j

-- indexed functor (1 index)
class IFunctor1 f where
  imap1 :: (s :-> t) -> (f s :-> f t)

-- indexed functor (2 index)
class IFunctor2 f where
  imap2 :: (s :--> t) -> (f s :--> f t)

-- dummy container type to store a solid result type
-- the shape should follow an indexed type
type family Dummy (x :: i -> k) :: * -> k

type Algebra1 f a = forall t. f ((Dummy f) a) t -> (Dummy f) a t
type Algebra2 f a = forall s t. f ((Dummy f) a) s t -> (Dummy f) a s t

cata1 :: IFunctor1 f => Algebra1 f a -> Mu1 f t -> (Dummy f) a t
cata1 alg = alg . imap1 (cata1 alg) . unRoll1

cata2 :: IFunctor2 f => Algebra2 f a -> Mu2 f s t -> (Dummy f) a s t
cata2 alg = alg . imap2 (cata2 alg) . unRoll2

И 2 примера структур для работы:

ExprF1 выглядит как обычная полезная вещь, прикрепляя встроенный тип к объектному языку.

ExprF2 придуман (дополнительный аргумент, который тоже отменяется (DataKinds)), просто чтобы узнать, способен ли "универсальный" cata2 обрабатывать эти фигуры.

-- our indexed type, which we want to use in an F-algebra (1 index)
data ExprF1 f t where
     ConstI1 :: Int -> ExprF1 f Int
     ConstB1 :: Bool -> ExprF1 f Bool
     Add1    :: f Int  -> f Int -> ExprF1 f Int
     Mul1    :: f Int  -> f Int -> ExprF1 f Int
     If1     :: f Bool -> f t -> f t -> ExprF1 f t
deriving instance (Show (f t), Show (f Bool)) => Show (ExprF1 f t)

-- our indexed type, which we want to use in an F-algebra (2 index)
data ExprF2 f s t where
     ConstI2 :: Int -> ExprF2 f Int True
     ConstB2 :: Bool -> ExprF2 f Bool True
     Add2    :: f Int True -> f Int True -> ExprF2 f Int True
     Mul2    :: f Int True -> f Int True -> ExprF2 f Int True
     If2     :: f Bool True -> f t True -> f t True -> ExprF2 f t True
deriving instance (Show (f s t), Show (f Bool t)) => Show (ExprF2 f s t)

-- mapper for f-algebra (1 index)
instance IFunctor1 ExprF1 where
  imap1 _    (ConstI1 x)  = ConstI1 x
  imap1 _    (ConstB1 x)  = ConstB1 x
  imap1 eval (x `Add1` y) = eval x `Add1` eval y
  imap1 eval (x `Mul1` y) = eval x `Mul1` eval y
  imap1 eval (If1 p t e)  = If1 (eval p) (eval t) (eval e)

-- mapper for f-algebra (2 index)
instance IFunctor2 ExprF2 where
  imap2 _    (ConstI2 x)  = ConstI2 x
  imap2 _    (ConstB2 x)  = ConstB2 x
  imap2 eval (x `Add2` y) = eval x `Add2` eval y
  imap2 eval (x `Mul2` y) = eval x `Mul2` eval y
  imap2 eval (If2 p t e)  = If2 (eval p) (eval t) (eval e)

-- turned into a nested expression
type Expr1 = Mu1 ExprF1

-- turned into a nested expression
type Expr2 = Mu2 ExprF2

-- dummy containers
newtype X1 x y = X1 x deriving Show
newtype X2 x y z = X2 x deriving Show

type instance Dummy ExprF1 = X1
type instance Dummy ExprF2 = X2


-- a simple example agebra that evaluates the expression
-- turning bools into 0/1    
alg1 :: Algebra1 ExprF1 Int
alg1 (ConstI1 x)            = X1 x
alg1 (ConstB1 False)        = X1 0
alg1 (ConstB1 True)         = X1 1
alg1 ((X1 x) `Add1` (X1 y)) = X1 $ x + y
alg1 ((X1 x) `Mul1` (X1 y)) = X1 $ x * y
alg1 (If1 (X1 0) _ (X1 e))  = X1 e
alg1 (If1 _ (X1 t) _)       = X1 t

alg2 :: Algebra2 ExprF2 Int
alg2 (ConstI2 x)            = X2 x
alg2 (ConstB2 False)        = X2 0
alg2 (ConstB2 True)         = X2 1
alg2 ((X2 x) `Add2` (X2 y)) = X2 $ x + y
alg2 ((X2 x) `Mul2` (X2 y)) = X2 $ x * y
alg2 (If2 (X2 0) _ (X2 e))  = X2 e
alg2 (If2 _ (X2 t) _)       = X2 t


-- simple helpers for construction
ci1 :: Int -> Expr1 Int
ci1 = Roll1 . ConstI1

cb1 :: Bool -> Expr1 Bool
cb1 = Roll1 . ConstB1

if1 :: Expr1 Bool -> Expr1 a -> Expr1 a -> Expr1 a
if1 p t e = Roll1 $ If1 p t e

add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
add1 x y = Roll1 $ Add1 x y

mul1 :: Expr1 Int -> Expr1 Int -> Expr1 Int
mul1 x y = Roll1 $ Mul1 x y

ci2 :: Int -> Expr2 Int True
ci2 = Roll2 . ConstI2

cb2 :: Bool -> Expr2 Bool True
cb2 = Roll2 . ConstB2

if2 :: Expr2 Bool True -> Expr2 a True-> Expr2 a True -> Expr2 a True
if2 p t e = Roll2 $ If2 p t e

add2 :: Expr2 Int True -> Expr2 Int True -> Expr2 Int True
add2 x y = Roll2 $ Add2 x y

mul2 :: Expr2 Int True -> Expr2 Int True -> Expr2 Int True
mul2 x y = Roll2 $ Mul2 x y


-- test case
test1 :: Expr1 Int
test1 = if1 (cb1 True)
            (ci1 3 `mul1` ci1 4 `add1` ci1 5)
            (ci1 2)

test2 :: Expr2 Int True
test2 = if2 (cb2 True)
            (ci2 3 `mul2` ci2 4 `add2` ci2 5)
            (ci2 2)


main :: IO ()
main = let (X1 x1) = cata1 alg1 test1
           (X2 x2) = cata2 alg2 test2
       in do print x1
             print x2

Выход:

17
17

Answer 1

Я написал доклад на эту тему под названием "Нарезка" в 2009 году. Это, безусловно, указывает на работу моих коллег из Стратклайда, Иоганна и Гани, по исходной семантике алгебры для GADT. Я использовал обозначение, которое SHE предоставляет для написания индексируемых данных типов, но это было приятно заменено историей "продвижения".

Ключевым моментом разговора, согласно моему комментарию, является систематичность использования только одного индекса, но использование факта, что его вид может варьироваться.

Так и есть (используя мои текущие предпочтительные имена "Goscinny and Uderzo")

type s :-> t = forall i. s i -> t i

class FunctorIx f where
  mapIx :: (s :-> t) -> (f s :-> f t)

Теперь вы можете показать FunctorIx закрыто под фиксированными точками. Ключ должен объединить два индексированных набора в один, который предлагает выбор индекса.

data Case (f :: i -> *) (g :: j -> *) (b :: Either i j) :: * where
  L :: f i -> Case f g (Left i)
  R :: g j -> Case f g (Right j)

(<?>) :: (f :-> f') -> (g :-> g') -> Case f g :-> Case f' g'
(f <?> g) (L x) = L (f x)
(f <?> g) (R x) = R (g x)

Теперь мы можем взять фиксированные точки функторов, чьи "содержащиеся элементы" означают "полезную нагрузку" или "рекурсивные подструктуры".

data MuIx (f :: (Either i j -> *) -> j -> *) :: (i -> *) -> j -> * where
  InIx :: f (Case x (MuIx f x)) j -> MuIx f x j

В результате мы можем mapIx над "полезной нагрузкой"...

instance FunctorIx f => FunctorIx (MuIx f) where
  mapIx f (InIx xs) = InIx (mapIx (f <?> mapIx f) xs)

... или написать катаморфизм над "рекурсивными субструктурами"...

foldIx :: FunctorIx f => (f (Case x t) :-> t) -> MuIx f x :-> t
foldIx f (InIx xs) = f (mapIx (id <?> foldIx f) xs)

... или оба сразу.

mapFoldIx :: FunctorIx f => (x :-> y) -> (f (Case y t) :-> t) -> MuIx f x :-> t
mapFoldIx e f (InIx xs) = f (mapIx (e <?> mapFoldIx e f) xs)

Радость FunctorIx в том, что он обладает такими великолепными свойствами закрытия благодаря возможности варьировать виды индексации. MuIx учитывает понятия полезной нагрузки и может быть повторен. Таким образом, существует стимул работать со структурированными индексами, а не с несколькими индексами.

Answer 2

Если я правильно понимаю, это как раз та проблема, которой занимается Иоганн и Гани "Первоначальная семантика алгебры достаточно!"

https://personal.cis.strath.ac.uk/neil.ghani/papers/ghani-tlca07.pdf

В частности, их hfold

Изменить: Для случая GADT, см. Их более позднюю статью "Основы для структурированного программирования с использованием GADT". Обратите внимание, что они сталкиваются с препятствием, которое можно устранить с помощью PolyKinds, которое у нас теперь есть: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.2948

Этот блог также может представлять интерес: http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html