Как обработать рекурсивный GADT с видом :: '[SomeDataKind]

Question

Я думаю, что это самый дальний в расширении системы типа Haskell, который я даже был, и я столкнулся с ошибкой, которую мне не удалось выяснить. Извините заранее за длину, это самый короткий пример, который я мог бы создать, который все еще иллюстрирует проблему, с которой я сталкиваюсь. У меня есть рекурсивную GADT чей вид является рекламируемый список, что-то вроде следующего:

GADT Определение

{-# LANGUAGE StandaloneDeriving #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 

data DataKind = A | B | C 

-- 'parts' should always contain at least 1 element which is enforced by the GADT. 
-- Lets call the first piece of data 'val' and the second 'subdata'. 
-- All data constructors have these 2 fields, although some may have 
-- additional fields which I've omitted for simplicity. 
data SomeData (parts :: [DataKind]) where 
    MkA :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('A ': subparts) 
    MkB :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('B ': subparts) 
    MkC :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('C ': subparts) 
deriving instance Show (SomeData parts) 

Проблема

То, что я пытаюсь сделать, это пройти данные и выполнить некоторые операции, например, распространить первый найденный вверх JustChar.

раздражающих недостающие функции - необходимы для следующего раздела

Теперь, потому что, видимо, нет поддержки синтаксиса записи для GADTs (https://ghc.haskell.org/trac/ghc/ticket/2595) вы должны написать их вручную, так вот они:

getVal :: SomeData parts -> Maybe Char 
getVal (MkA val _) = val 
getVal (MkB val _) = val 
getVal (MkC val _) = val 

-- The lack of record syntax for GADTs is annoying. 
updateVal :: Maybe Char -> SomeData parts -> SomeData parts 
updateVal val (MkA _val sub) = MkA val sub 
updateVal val (MkB _val sub) = MkB val sub 
updateVal val (MkC _val sub) = MkC val sub 

-- really annoying... 
getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest) 
getSubData (MkA _ sub) = sub 
getSubData (MkB _ sub) = sub 
getSubData (MkC _ sub) = sub 

Test Data

Итак, что я хочу сделать. Пройдите вниз по структуре сверху, пока не найду значение Just. Поэтому, учитывая следующие начальные значения:

a :: SomeData '[ 'A ] 
a = MkA (Just 'A') Nothing 

b :: SomeData '[ 'B ] 
b = MkB (Just 'B') Nothing 

c :: SomeData '[ 'C ] 
c = MkC (Just 'C') Nothing 

bc :: SomeData '[ 'B, 'C ] 
bc = MkB Nothing (Just c) 

abc :: SomeData '[ 'A, 'B, 'C ] 
abc = MkA Nothing (Just bc) 

Ожидаемый результат

Я хотел бы иметь что-то вроде этого:

> abc 
MkA Nothing (Just (MkB Nothing (Just (MkC (Just 'C') Nothing)))) 
> propogate abc 
MkA (Just 'C') (Just (MkB (Just 'C') (Just (MkC (Just 'C') Nothing)))) 

Предыдущие попытки

Я сделал несколько уколы на нем, сначала с регулярной функцией:

propogate sd = 
    case getVal sd of 
     Just _val -> 
      sd 
     Nothing -> 
      let 
       newSubData = fmap propogate (getSubData sd) 
       newVal = join . fmap getVal $ newSubData 
      in 
       updateVal newVal sd 

Это дает ошибку:

Broken.hs:(70,1)-(81,35): error: … 
    • Occurs check: cannot construct the infinite type: rest ~ p : rest 
     Expected type: SomeData rest -> SomeData (p : rest) 
     Actual type: SomeData (p : rest) -> SomeData (p : rest) 
    • Relevant bindings include 
     propogate :: SomeData rest -> SomeData (p : rest) 
      (bound at Broken.hs:70:1) 
Compilation failed. 

Я также попробовал класс типов и пытается соответствовать по структуре:

class Propogate sd where 
    propogateTypeClass :: sd -> sd 

-- Base case: We only have 1 element in the promoted type list. 
instance Propogate (SomeData parts) where 
    propogateTypeClass sd = sd  

-- Recursie case: More than 1 element in the promoted type list. 
instance Propogate (SomeData (p ': parts)) where 
    propogateTypeClass sd = 
     case getVal sd of 
      Just _val -> 
       sd 
      Nothing -> 
       let 
        -- newSubData :: Maybe subparts 
        -- Recurse on the subdata if it exists. 
        newSubData = fmap propogateTypeClass (getSubData sd) 
        newVal = join . fmap getVal $ newSubData 
       in 
        updateVal newVal sd 

Это приводит к ошибке:

Broken.hs:125:5-26: error: … 
    • Overlapping instances for Propogate (SomeData '['A, 'B, 'C]) 
     arising from a use of ‘propogateTypeClass’ 
     Matching instances: 
     instance Propogate (SomeData parts) 
      -- Defined at Broken.hs:91:10 
     instance Propogate (SomeData (p : parts)) 
      -- Defined at Broken.hs:95:10 
    • In the expression: propogateTypeClass abc 
     In an equation for ‘x’: x = propogateTypeClass abc 
Compilation failed. 

Я также пробовал сочетания совпадений на SomeData '[] и SomeData '[p] безрезультатно.

Я надеюсь, что мне не хватает чего-то простого, но я не нашел документацию в любом месте о том, как обрабатывать структуру, подобную этой, и я нахожусь в пределах моего понимания, если система типа Haskell, на данный момент в любом случае:).Еще раз, извините за длинный пост и любая помощь будет принята с благодарностью :)

Answer 1

Ошибка, которую вы получаете, - это красная сельдь - GHC не может выводить типы функций на GADT. Вы должны дать ему тип подписи, чтобы увидеть реальную ошибку:

propogate :: SomeData x -> SomeData x 
.... 

Это дает ошибку:

* Couldn't match type `x' with `p0 : parts0' 
    `x' is a rigid type variable bound by 
    the type signature for: 
     propogate :: forall (x :: [DataKind]). SomeData x -> SomeData x 
    Expected type: SomeData (p0 : parts0) 
    Actual type: SomeData x 

Если это не ясно, это сообщение об ошибке говорит, что мы утверждаем, что тип arguement к SomeData - это просто переменная (т. Е. Мы ничего не знаем об этом, кроме ее вида), но использование некоторых функций внутри propogate требует, чтобы она представляла собой вид p0 : parts0 для некоторых типов p0 : parts0.

Однако, вы заявляете в начале:

'parts' should always contain at least 1 element which is enforced by the GADT.

но компилятор не знает! Вы должны сказать об этом, и обычно это делается путем сопоставления шаблонов в конструкторе GADT, который привносит в сферу применения равенство типа. Ваша единственная проблема заключается в том, что вам придется сопоставлять три конструктора, каждый из которых будет иметь идентичный код. Решение состоит в том, чтобы удалить дубликаты из вашего типа данных:

data SomeData (parts :: [DataKind]) where 
    Mk :: SDataKind s -> Maybe Char -> Maybe (SomeData subparts) -> SomeData (s ': subparts) 

data SDataKind (x :: DataKind) where 
    SA :: SDataKind A 
    SB :: SDataKind B 
    SC :: SDataKind C 

Пакеты, как singletons будет генерировать тип SDataKind и связанные с ним функции по типу автоматически.

Все функции вашего «рекорд» значительно упрощаются:

getVal :: SomeData parts -> Maybe Char 
getVal (Mk _ v _) = v 

updateVal :: Maybe Char -> SomeData parts -> SomeData parts 
updateVal val (Mk t _val sub) = Mk t val sub 

getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest) 
getSubData (Mk _ _ sub) = sub 

И теперь, для того, чтобы получить функцию для typecheck (так как это действительно правильно семантически), все, что вам нужно сделать, это сопоставление с образцом на конструктор:

propogate :: SomeData x -> SomeData x 
propogate sd@Mk{} = 
    .... -- unchanged 

Обратите внимание, что код идентичен, за исключением добавления сигнатуры типа и @Mk{} после переменного шаблона sd.

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

---

Также обратите внимание, что вы не потеряете любой общности в SomeData - если вы хотите конкретные показатели, чтобы иметь дополнительную информацию, вы просто добавить еще одно поле, индексированную на part.Вы даже можете встроить сложную логику внутри дополнительного поля, как SDataKind поле позволяет шаблон матч по индексу по желанию:

data SomeData (parts :: [DataKind]) where 
    Mk :: SDataKind s 
    -> DataPart s 
    -> Maybe Char 
    -> Maybe (SomeData subparts) 
    -> SomeData (s ': subparts) 

type family (==?) (a :: k) (b :: k) :: Bool where 
    a ==? a = 'True 
    a ==? b = 'False 

-- Example - an additional field for only one index, without duplicating 
-- the constructors for each index 
data DataPart x where 
    Nil :: ((x ==? 'A) ~ 'False) => DataPart x 
    A_Data :: Integer -> DataPart A 

---

Наконец, если вы хотите, чтобы тащиться вдоль первоначального курса, вы может сделать это, но источник дублирования кода должен стать весьма очевидным:

partsUncons :: SomeData ps0 -> (forall p ps . (ps0 ~ (p : ps)) => r) -> r 
partsUncons MkA{} x = x 
partsUncons MkB{} x = x 
partsUncons MkC{} x = x 

propogate :: SomeData x -> SomeData x 
propogate sd = partsUncons sd $ 
    .... -- unchanged 

Answer 2

Это может показаться немного шаблонный-иш, но если вы просто выписать три случая из propagate, то это может быть сделано просто (если бит многословный):

import Control.Monad (mplus) 
import Control.Arrow (second) 

propagate' :: (Maybe Char -> Maybe (SomeData ps) -> SomeData ps') 
      -> Maybe Char -> Maybe (SomeData ps) -> (Maybe Char, SomeData ps') 
propagate' mk c ds = (c'', mk c'' ds') 
    where 
    (c', ds') = maybe (Nothing, Nothing) (second Just . propagate) ds 
    c'' = c `mplus` c' 

propagate :: SomeData ps -> (Maybe Char, SomeData ps) 
propagate (MkA c ds) = propagate' MkA c ds 
propagate (MkB c ds) = propagate' MkB c ds 
propagate (MkC c ds) = propagate' MkC c ds