Is it possible to write a type-level function that returns True
if one type-level list contains another type-level list?
Here is my attempt:
{-# 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
It works for simple cases:
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’
But what about cases like this?
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)
The trouble is that you've defined your subset type family by induction on the structure of the contained list, but you're passing in a totally polymorphic (unknown) list whose structure is a mystery to GHC. You might think that GHC would be able to use induction anyway, but you'd be wrong. In particular, just as every type has undefined values, so every kind has "stuck" types. A notable example, which GHC uses internally and exports through (IIRC) GHC.Exts
:
{-# LANGUAGE TypeFamilies, PolyKinds #-}
type family Any :: k
The Any
type family is in every kind. So you could have a type-level list Int ': Char ': Any
, where Any
is used at kind [*]
. But there's no way to deconstruct the Any
into ':
or []
; it doesn't have any such sensible form. Since type families like Any
exist, GHC cannot safely use induction on types the way you wish.
If you want induction to work properly over type lists, you really need to use singletons or similar as Benjamin Hodgson suggests. Rather than passing just the type-level list, you need to pass also a GADT giving evidence that the type-level list is constructed properly. Recursively destructing the GADT performs induction over the type-level list.
The same sorts of limitations hold for type-level natural numbers.
data Nat = Z | S Nat
type family (x :: Nat) :+ (y :: Nat) :: Nat where
'Z :+ y = y
('S x) :+ y = 'S (x :+ y)
data Natty (n :: Nat) where
Zy :: Natty 'Z
Sy :: Natty n -> Natty ('S n)
You might wish to prove
associative :: p1 x -> p2 y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))
but you can't, because this requires induction on x
and y
. You can, however, prove
associative :: Natty x -> Natty y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))
with no trouble.
There seems to be an obsession with Boolean type families that's endemic to the Haskell community. Don't use them! You're making more work for yourself than necessary when it comes to using the result of such a test.
Subset-ness is a proposition that may be proved with information-rich evidence. Here's one simple way of designing such evidence. First, the type of proofs that an element can be found in a list:
data Elem xs x where
Here :: Elem (x ': xs) x
There :: Elem xs x -> Elem (y ': xs) x
Elem
is structured like a natural number (compare There (There Here)
with S (S Z)
) but with more types. To prove that an element is in a list you give its index.
data All f xs where
Nil :: All f '[]
Cons :: f x -> All f xs -> All f (x ': xs)
All
is a proof that a given predicate applies to every element of a list. It's structured as a list of proofs of f
.
Now the type of proofs that a list is a subset of another list is easy to write down using these bits of machinery.
type IsSubset xs ys = All (Elem ys) xs
IsSubset
is represented as a list of proofs that each element of xs
can be found in ys
.
You can automate proof search for IsSubset
values by hacking the type class system, but that's another post.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With