Extract a Maybe from a heterogeneous collection

Question

I have a project where I define a "heterogenous list" like the following. I'm not sure what this trick is called but I've found it to be useful:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

import Data.Kind (Type)

data (a :: Type) :> (b :: Type) = a :> b
  deriving Show
infixr :>

With this, I can write arbitrarily long lists of values like this:

val :: Int :> Bool :> String
val = 42 :> True :> "asdf"

I'm trying to write a function to test if such a value contains a given type, and if so extract it as a Maybe. For example,

-- | getInt (42 :> "asdf") -> Just 42
-- | getInt (True :> "asdf") -> Nothing
getInt :: a :> b -> Maybe Int
getInt _ = ???

But I haven't figured out a way to write functions like this. I tried using cast from Data.Typeable, but ran into various problems trying to destructure at the type level.

Answer 1

You can do this with Type.Reflection, as per @chi's comment (see below).

However, you might find it easier to use a more traditional list type with both a "cons" and a "nil" constructor and embedded Typeable instances:

{-# LANGUAGE DataKinds #-}

infixr 5 :>
data HList ts where
  (:>) :: (Typeable t) => t -> HList ts -> HList (t ': ts)
  Nil :: HList '[]

Note that you can maintain most of the ergonomics of the original with a few cleverly named type families and aliases:

{-# LANGUAGE UndecidableInstances #-}

type family (:>) t ts where
  t :> HList ts = HList (t ': ts)
  t :> x = TypeError (Text "(:>) type ended with " :<>: ShowType x
                     :<>: Text " instead of Nil")
type Nil = HList '[]

This allows you to write:

val :: Int :> Bool :> String :> Nil
val = 42 :> True :> "asdf" :> Nil

because the :> and Nil in types are type families/aliases which expand to a valid HList type, and the :> and Nil in expressions are the constructors for the corresponding HList type.

With this in place, it's easy to define getInt with just cast from Data.Typeable:

import Data.Typeable

getInt :: HList ts -> Maybe Int
getInt (x :> xs) | Just a <- cast x = Just a
                 | otherwise = getInt xs
getInt Nil = Nothing

Critically, the extra Nil constructor eliminates the need to try to distinguish at the type level if the right-hand side of a :> constructor is a final value or "more list".

This will generally be much more pleasant to work with in all sorts of ways at the relatively small cost of a little :> Nil boilerplate.

A full example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module KindList2 where

import Data.Typeable
import GHC.TypeError

infixr :>
type family (:>) t ts where
  t :> HList ts = HList (t ': ts)
  t :> x = TypeError (Text "(:>) type ended with " :<>: ShowType x
                     :<>: Text " instead of Nil")
type Nil = HList '[]

data HList ts where
  (:>) :: Typeable t => t -> HList ts -> HList (t ': ts)
  Nil :: HList '[]

getInt :: HList ts -> Maybe Int
getInt (x :> xs) | Just a <- cast x = Just a
                 | otherwise = getInt xs
getInt Nil = Nothing

v1 :: Int :> Bool :> String :> Nil
v1 = 42 :> True :> "asdf" :> Nil
v2 :: String :> Int :> String :> Nil
v2 = "between" :> 2 :> "strings" :> Nil
v3 :: String :> Int :> Nil
v3 = "sweet" :> 16 :> Nil
v4 :: String :> Bool :> Nil
v4 = "contains Int = " :> False :> Nil

main = do
  print $ getInt v1
  print $ getInt v2
  print $ getInt v3
  print $ getInt v4

which produces the output:

λ> main
Just 42
Just 2
Just 16
Nothing

However, if you want to stick with your :>-only approach, then Data.Typeable is insufficient because it can't be "decomposed" at the type level. You've probably observed that it's easy enough to write:

import Data.Kind (Type)
import Data.Typeable

data (a :: Type) :> (b :: Type) = a :> b
  deriving (Show)
infixr :>

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b) | Just x <- cast a = Just x
                | Just x <- cast b = Just x

which can successfully extract the Int from Int :> Bool and Bool :> Int, but there's no straightforward way to recurse using cast:

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b) | Just x <- cast a = Just x
                | Just x <- cast b = Just x
                | Just rest <- cast b = getInt rest   -- ERROR

Because even though the cast b can successfully cast b to a c :> d, there's no way to get the required Typeable c and Typeable d constraints from Typeable b.

However, if you use Type.Reflection instead, it's possible. Note that I've used explicit export lists here, but basically I've used cast from Data.Typeable for convenience, and everything else (including the Typeable type itself) needs to come from `Type.Reflection).

import Data.Typeable (cast)
import Type.Reflection (Typeable, pattern App, pattern HRefl, pattern TypeRep,
                        typeOf, eqTypeRep, withTypeable,)


getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b)

  -- handle `Int :> a`
  | Just x <- cast a = Just x

  -- handle `x :> (y :> z)`
  --   extract type (of right-hand side) as:  c `op` d
  | App (App op c) d <- typeOf b
  --   check op ~ (:>)
  , Just HRefl <- eqTypeRep op (TypeRep @(:>))
  --   extract Typeable c, Typeable d, and recurse
    = withTypeable c $ withTypeable d $ getInt b

  -- handle `x :> Int`
  | Just x <- cast b = Just x

  -- handle remaining cases
  | otherwise = Nothing

The full example:

{-# LANGUAGE GADTs #-}            -- needed to avoid "fragile" guard bindings
{-# LANGUAGE PatternSynonyms #-}  -- only needed for import list
{-# LANGUAGE TypeOperators #-}

module KindList where

import Data.Typeable (cast)
import Type.Reflection (Typeable, pattern App, pattern HRefl, pattern TypeRep,
                        typeOf, eqTypeRep, withTypeable,)

data a :> b = a :> b deriving (Show)
infixr :>

getInt :: (Typeable a, Typeable b) => a :> b -> Maybe Int
getInt (a :> b)
  | Just x <- cast a = Just x
  | App (App op c) d <- typeOf b
  , Just HRefl <- eqTypeRep op (TypeRep @(:>))
    = withTypeable c $ withTypeable d $ getInt b
  | Just x <- cast b = Just x
  | otherwise = Nothing

v1 :: Int :> Bool :> String
v1 = 42 :> True :> "asdf"
v2 :: String :> Int :> String
v2 = "between" :> 2 :> "strings"
v3 :: String :> Int
v3 = "sweet" :> 16
v4 :: String :> Bool
v4 = "contains Int = " :> False

main = do
  print $ getInt v1
  print $ getInt v2
  print $ getInt v3
  print $ getInt v4

Answer 2

I guess you can do something like this. I use the standard (,) instead of your (:>), but only to keep the code minimal; there's nothing fundamental that can't be ported to your type.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ViewPatterns #-}

import Control.Applicative
import Type.Reflection

get :: forall needle haystack. (Typeable needle, Typeable haystack) =>
    haystack -> Maybe needle
get haystack = case typeOf haystack of
    (eqTypeRep (typeRep @needle) -> Just HRefl)
        -> Just haystack
    App (App (eqTypeRep (typeRep @(,)) -> Just HRefl) a) b
        ->  withTypeable a (get (fst haystack))
        <|> withTypeable b (get (snd haystack))
    _ -> Nothing

Try it in ghci:

> get @Integer (42, (True, "asdf"))
Just 42
> get @Integer (True, (42, "asdf"))
Just 42
> get @Integer (True, ("asdf", 42))
Just 42
> get @Integer (True, ('w', "asdf"))
Nothing

Actually, this recurses on both sides of the tuple, so it works for some things you might not have imagined; e.g. get @Integer (("asdf", 42), True) also returns Just 42. This can be prevented if desired; simply perform another typerep equality check in the first argument to <|> instead of recursing.

This uses withTypeable, but then immediately pattern matches on the associated typeRep. If science goes too far and you find you care about the performance of this abomination, you can avoid that, making O(1) calls to typeRep, like this.

get :: forall needle haystack. (Typeable needle, Typeable haystack) =>
    haystack -> Maybe needle
get = go typeRep where
    go :: forall haystack. TypeRep haystack -> haystack -> Maybe needle
    go (eqTypeRep needleTy -> Just HRefl) needle = Just needle
    go (App (App (eqTypeRep pairTy -> Just HRefl) aTy) bTy) (a, b)
        = go aTy a <|> go bTy b
    go _ _ = Nothing

    needleTy :: TypeRep needle
    needleTy = typeRep

    pairTy :: TypeRep (,)
    pairTy = typeRep