Comprobando si una lista de nivel de tipo contiene otra
¿Es posible escribir una función de nivel de tipo que devuelvaTrue
si una lista de nivel de tipo contiene otra lista de nivel de tipo?
Aquí está mi intento:
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module TypePlayground where
import Data.Type.Bool
type family InList (x :: *) (xs :: [*]) where
InList x '[] = 'False
InList x (x ': xs) = 'True
InList x (a ': xs) = InList x xs
type family ListContainsList (xs :: [*]) (ys :: [*]) where
ListContainsList xs (y ': ys) = InList y xs && ListContainsList xs ys
ListContainsList xs '[] = 'True
Funciona para casos simples:
data A
data B
data C
test1 :: (ListContainsList '[A, B, C] '[C, A] ~ 'True) => ()
test1 = ()
-- compiles.
test2 :: (ListContainsList '[A, B, C] '[B, C, A] ~ 'True) => ()
test2 = ()
-- compiles.
test3 :: (ListContainsList (A ': B ': '[C]) (B ': A ': '[C]) ~ 'True) => ()
test3 = ()
-- compiles.
test4 :: (ListContainsList '[A, C] '[B, C, A] ~ 'True) => ()
test4 = ()
-- Couldn't match type ‘'False’ with ‘'True’
¿Pero qué pasa con casos como este?
test5 :: (ListContainsList (A ': B ': a) a ~ 'True) => ()
test5 = ()
-- Should compile, but fails:
-- Could not deduce (ListContainsList (A : B : a0) a0 ~ 'True)
-- from the context (ListContainsList (A : B : a) a ~ 'True)