Tworzenie całkowicie zależnej konkatenacji

10

Dobrym prawdziwym faktem na temat konkatenacji jest to, że jeśli znam dowolne dwie zmienne w równaniu:

a ++ b = c

Więc znam trzeci.

Chciałbym uchwycić ten pomysł w swoim własnym konkat, więc używam zależności funkcjonalnej.

{-# Language DataKinds, GADTs, FlexibleContexts, FlexibleInstances, FunctionalDependencies, KindSignatures, PolyKinds, TypeOperators, UndecidableInstances #-}
import Data.Kind (Type)

class Concatable
   (m  :: k -> Type)
   (as :: k)
   (bs :: k)
   (cs :: k)
   | as bs -> cs
   , as cs -> bs
   , bs cs -> as
   where
     concat' :: m as -> m bs -> m cs

Teraz wyczaruję listę heterogeniczną w ten sposób:

data HList ( as :: [ Type ] ) where
  HEmpty :: HList '[]
  HCons  :: a -> HList as -> HList (a ': as)

Ale kiedy próbuję zadeklarować je jako Concatableproblem

instance Concatable HList '[] bs bs where
  concat' HEmpty bs = bs
instance
  ( Concatable HList as bs cs
  )
    => Concatable HList (a ': as) bs (a ': cs)
  where
    concat' (HCons head tail) bs = HCons head (concat' tail bs)

Nie spełniam mojej trzeciej zależności funkcjonalnej. A raczej kompilator uważa, że ​​nie. Jest tak, ponieważ kompilator uważa, że ​​w naszym drugim przypadku może tak być bs ~ (a ': cs). I może tak być, jeśli Concatable as (a ': cs) cs.

Jak mogę dostosować moje wystąpienia, aby wszystkie trzy zależności były spełnione?

Sriotchilism O'Zaic
źródło
1
Wydaje się bs cs -> as, że kluczowym problemem jest to , że potrzebujemy nielokalnych informacji na temat bsi csdecydować, czy aspowinny to być minusy czy zero. Musimy dowiedzieć się, jak reprezentować te informacje; jaki kontekst dodalibyśmy do podpisu typu, aby zagwarantować go, gdy nie można go bezpośrednio wywnioskować?
luqui
3
Aby rozwinąć to, co powiedział luqui: wyobraź sobie, że wiemy bsi cschcemy wykorzystać fundep, czyli chcemy zrekonstruować as. Aby to zrobić w sposób deterministyczny, oczekujemy, że będziemy w stanie zatwierdzić jedną instancję i zastosować się do tego przepisu. Konkretnie, załóż bs = (Int ': bs2)i cs = (Int ': cs2). Którą instancję wybieramy? Jest możliwe, że taki Intw cspochodzi z bs(i asjest pusta). Możliwe jest również, że pochodzi z (niepuste) as, i Intpojawi się ponownie cspóźniej. Musimy wniknąć głębiej, csaby wiedzieć, a GHC tego nie zrobi.
chi
1
Mówiąc z grubsza, GHC zaakceptuje fundeps, które można udowodnić za pomocą prostej formy indukcji z instancji. Tutaj jeden z nich wymaga udowodnienia (przynajmniej tak się wydaje) pewnego rodzaju podwójnej indukcji, a kompilator nie posunie się tak daleko.
chi

Odpowiedzi:

10

Tak więc, jak sugerują komentarze, GHC nie rozwiąże tego samodzielnie, ale możemy pomóc przy odrobinie programowania na poziomie czcionki. Przedstawmy trochę TypeFamilies. Wszystkie te funkcje są dość prostymi tłumaczeniami manipulacji listami podniesionymi do poziomu typu:

-- | This will produce the suffix of `cs` without `as`
type family DropPrefix (as :: [Type]) (cs :: [Type]) where
  DropPrefix '[] cs = cs
  DropPrefix (a ': as) (a ': cs) = DropPrefix as cs

-- Similar to the logic in the question itself: list concatenation. 
type family Concat (as :: [Type]) (bs :: [Type]) where
  Concat '[] bs = bs
  Concat (head ': tail) bs = head ': Concat tail bs

-- | Naive list reversal with help of concatenation.
type family Reverse (xs :: [Type]) where
  Reverse '[] = '[]
  Reverse (x ': xs) = Concat (Reverse xs) '[x]

-- | This will produce the prefix of `cs` without `bs`
type family DropSuffix (bs :: [Type]) (cs :: [Type]) where
  DropSuffix bs cs = Reverse (DropPrefix (Reverse bs) (Reverse cs))

-- | Same definition of `HList` as in the question
data HList (as :: [Type]) where
  HEmpty :: HList '[]
  HCons :: a -> HList as -> HList (a ': as)

-- | Definition of concatenation at the value level
concatHList :: (cs ~ Concat as bs) => HList as -> HList bs -> HList cs
concatHList HEmpty bs = bs
concatHList (HCons head tail) bs = HCons head (concatHList tail bs)

Dzięki tym narzędziom, które mamy do dyspozycji, możemy faktycznie osiągnąć cel godzinowy, ale najpierw zdefiniujmy funkcję o pożądanych właściwościach:

  • Możliwość wnioskowania na cspodstawie asibs
  • Możliwość wnioskowania na aspodstawie bsics
  • Możliwość wnioskowania na bspodstawie asics

Voila:

concatH ::
     (cs ~ Concat as bs, bs ~ DropPrefix as cs, as ~ DropSuffix bs cs)
  => HList as
  -> HList bs
  -> HList cs
concatH = concatHList

Przetestujmy to:

foo :: HList '[Char, Bool]
foo = HCons 'a' (HCons True HEmpty)

bar :: HList '[Int]
bar = HCons (1 :: Int) HEmpty
λ> :t concatH foo bar
concatH foo bar :: HList '[Char, Bool, Int]
λ> :t concatH bar foo
concatH bar foo :: HList '[Int, Char, Bool]

I wreszcie cel końcowy:

class Concatable (m :: k -> Type) (as :: k) (bs :: k) (cs :: k)
  | as bs -> cs
  , as cs -> bs
  , bs cs -> as
  where
  concat' :: m as -> m bs -> m cs

instance (cs ~ Concat as bs, bs ~ DropPrefix as cs, as ~ DropSuffix bs cs) =>
         Concatable HList as bs cs where
  concat' = concatH
λ> :t concat' HEmpty bar
concat' HEmpty bar :: HList '[Int]
λ> :t concat' foo bar
concat' foo bar :: HList '[Char, Bool, Int]
λ> :t concat' bar foo
concat' bar foo :: HList '[Int, Char, Bool]
lehins
źródło
3
Dobra robota! Podejrzewałem nawet, że może to być niemożliwe, ale rozwiązaliście to w sposób przejrzysty i elegancki.
luqui
Dziękuję, @luqui
lehins,