I’m playing around with heterogeneous list types, vaguely inspired by the Vinyl librairies records.
Most of it works fine, but I struggle a bit finding out good ways to map over the heterogeneous types in the list—understandably because GHC somehow needs to know what functions I can apply to them—and to filter out certain types and convert to a homogeneous regular list.
Here is what I have, with the latter functions just pseudocode because I don’t know how to best implement them:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
module Main where
data HL :: [*] -> * where
HNil :: HL '[]
(:&) :: !r -> !(HL rs) -> HL (r ': rs)
infixr 7 :&
a :: HL '[Double, String, Double]
a = 3.0 :& "hey" :& 1.0 :& HNil
-- how can I implement the following "filter", "convert" and "mult" functions?
b :: HL '[Double, Double]
b = filter (Proxy @Double) a
c :: [Double]
c = convert b
mult :: HL xs -- where all elements x of xs fullfill the Num x constraint.
mult x = hlmap (*2) x
You can take a look at Typeable. First add a constraint to your constructor:
data HL :: [*] -> * where
HNil :: HL '[]
(:&) :: Typeable r => !r -> !(HL rs) -> HL (r ': rs)
(or add another typeclass AllTypeable rs that ensures all types in typelevel list rs are typeable, and add it to context to your functions).
Then you should be able to write a function like
mapHL :: (forall a. Typeable a => a -> Maybe b) -> HL rs -> [b]
mapHL _ HNil = []
mapHL f (x :& xs) = case f x of
Nothing -> mapHL f xs
Just v -> v : mapHL f xs
For instance, if you want to filter out doubles:
import Data.Typeable (cast)
castDouble :: Typeable a => a -> Maybe Double
castDouble = cast
b :: [Double]
b = mapHL castDouble a -- or just mapHL (cast @_ @Double) a
Note that writing a function that takes a HL and returns a HL is a different pair of shoes.
Thanks for your answer @Swordlash that’s super helpful. Could you elaborate a bit more on the “different pair of shoes”? Any link that I could follow to see examples of how that is done?
What I mean is for GHC to be able to typecheck your code, it has to be sure argument and return types are correct. So, it’s hard to write a function like
mapHL :: (something) -> HL rs -> HL rs'
What you need to write is a separate typeclass / type family for rs', for GHC to know what to expect. What complicates things more is no notion of “type inequality”:
import Type.Reflection
import Data.Proxy
import Unsafe.Coerce
type family FilterTypes b rs where
FilterTypes b '[] = '[]
FilterTypes b (b ': rest) = b ': FilterTypes b rest
FilterTypes b (a ': rest) = FilterTypes b rest
filterElems :: forall b rs. Typeable b => Proxy b -> HL rs -> HL (FilterTypes b rs)
filterElems _ HNil = HNil
filterElems p (x :& xs) = case eqTypeRep (typeOf x) (typeRep @b) of
Just HRefl -> x :& filterElems p xs
-- ^ here GHC knows that type of x is b, `HRefl` is a witness of it
Nothing -> unsafeCoerce $ filterElems p xs
-- ^ here compiler does not know a /= b, it just knows it cannot prove a == b
-- that's why we need to unsafeCoerce, maybe there is a better way
a :: HL '[Double, String, Double]
a = 3.0 :& "hey" :& 1.0 :& HNil
b :: HL '[Double, Double]
b = filterElems (Proxy @Double) a
main = pure ()