Heterogeneous lists: how to map over, filter and convert?

Learn
#1

Hi all,

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

Any ideas how to best do this?

#2

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.

2 Likes
#3

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?

#4

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 ()
2 Likes
#5

In general you’re gonna need a separate type family or typeclass for all kinds of transformations you come up with.