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

Question

Недавно я немного узнал о F-алгебрах: https://www.fpcomplete.com/user/bartosz/understanding-algebras. Я хотел поднять эту функциональность на более продвинутые типы (индексированные и более высокоподобные). Кроме того, я проверил «Предоставление Haskell Promotion» (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

я написал доклад на эту тему под названием "Slicing It" в 2009 году безусловно, указывает на работу моих коллег из Strathclyde, Йоханна и Гани, по семантике исходной алгебры для GADT.Я использовал обозначение, которое SHE предусматривает запись индексированных данных типов, но это было приятно заменено «продвижением».

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

Так на самом деле, мы (используя мои текущие предпочитаемые имена «Gościnny и 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

Edit: Для случая GADT, увидеть их позже документ "Основы структурированных вычислениям GADTs". Обратите внимание, что они сталкиваются с препятствием, которое может быть решена с помощью 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