[Haskell-cafe] Type-level list "elem" inference

[Adam Gundry]

Hi Tom,

One way is to write type families returning constraints, like this:


type family IsSubset (as :: [Symbol]) (bs :: [Symbol]) :: Constraint where
   IsSubset '[]       bs = ()
   IsSubset (a ': as) bs = (IsElem a bs, IsSubset as bs)

type family IsElem (a :: Symbol) (bs :: [Symbol]) :: Constraint where
   IsElem a (a ': bs) = ()
   IsElem a (b ': bs) = IsElem a bs
-- For bonus points in GHC 8.0:
-- IsElem a '[] = TypeError (Text a :<>: Text " not an element!")


Then you can write:


foo :: IsSubset '["foo", "bar"] args => Proxy args -> Int
foo args = bar args

bar :: IsElem "foo" args => Proxy args -> Int
bar args = undefined


This is less expressive than your approach in other ways, though (e.g.
one can't talk about negative constraints very easily).

Hope this helps,

Adam


On 05/03/16 19:34, amindfv at gmail.com wrote:
> So I've got some code that looks like:
> 
> {-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies, KindSignatures, TypeOperators #-}
> 
> import Data.Proxy
> import GHC.TypeLits
> 
> type family IsSubset (as :: [Symbol]) (bs :: [Symbol]) where
>    IsSubset as bs = IsSubsetPrime as bs bs
> 
> type family IsSubsetPrime (as :: [Symbol]) bs bs' where
>    IsSubsetPrime as '[] bs' = 'False
>    IsSubsetPrime '[] bs bs' = 'True
>    IsSubsetPrime (a ': as) (a ': bs) bs' =
> IsSubsetPrime as bs' bs'
>    IsSubsetPrime (a ': as) (b ': bs) bs' = IsSubsetPrime (a ': as) bs bs'
> 
> 
> 
> This lets me write functions like:
> 
> 
> foo :: (IsSubset '["foo", "bar"] args ~ 'True) => Proxy args -> Int
> foo args = undefined
> 
> 
> I've also got a type family:
> 
> 
> type family IsElem (a :: Symbol) (bs :: [Symbol]) where
>    IsElem a (a ': bs) = 'True
>    IsElem a (b ': bs) = IsElem a bs
>    IsElem a '[] = 'False
> 
> 
> This lets me write functions like:
> 
> bar :: (IsElem "foo" args ~ 'True) => Proxy args -> Int
> bar args = undefined
> 
> 
> The problem comes when I want to use "bar args" in the definition of "foo args" -- even though it's clear to me that ["foo","bar"] being a subset of args implies that "foo" is an element of args, I haven't written "IsElem" or "IsSubset" in a way that it's clear to the compiler.
> 
> Is there a way to write IsElem and IsSubset so they "compose"?
> 
> Thanks!
> Tom


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/