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@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/