Type-level list "elem" inference

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Type-level list "elem" inference

amindfv
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type-level list "elem" inference

Adam Gundry-2
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, [hidden email] 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/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe