Сложите разнородное, время компиляции, список

Отвечая на ваш комментарий:

На самом деле, я могу сделать, если я могу фильтровать разнородный список по типу. Это возможно?

Вы можете отфильтровать гетерогенный список по типу, если добавите ограничение Typeable к b.

Основная идея заключается в том, что мы будем использовать Data.Typeable. >cast :: (Typeable a, Typeable b) => a -> Maybe b чтобы определить, относится ли каждый элемент в списке к определенному типу. Это потребует ограничения Typeable для каждого элемента в списке. Вместо того, чтобы создавать новый тип списка с этим встроенным ограничением, мы сделаем возможность проверять, соответствуют ли All типов в списке какому-либо ограничению.

Наша цель — заставить следующую программу выводить [True,False], отфильтровывая разнородный список только по его Bool элементам. Я постараюсь разместить языковые расширения и импорт с первым фрагментом, для которого они необходимы.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

example :: HList (Bool ': String ': Bool ': String ': '[])
example = HCons True $ HCons "Jack" $ HCons False $ HCons "Jill" $ HNil

main = do
    print (ofType example :: [Bool])

HList вот довольно стандартное определение разнородного списка в haskell с использованием DataKinds

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data HList (l :: [*]) where
    HCons :: h -> HList t -> HList (h ': t)
    HNil :: HList '[]

Мы хотим написать ofType с подписью типа "если All вещей в разнородном списке Typeable, получить список этих вещей определенного Typeable типа.

import Data.Typeable

ofType :: (All Typeable l, Typeable a) => HList l -> [a]

Для этого нам нужно разработать понятие All вещей в списке типов, удовлетворяющих некоторым ограничениям. Мы будем хранить словари для удовлетворенных ограничений в GADT, который либо захватывает словарь ограничения головы и ограничения для All хвоста, либо доказывает, что список пуст. Список типов удовлетворяет ограничению для All его элементов, если мы можем захватить для него словари.

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE ConstraintKinds #-}

-- requires the constraints† package.
-- Constraint is actually in GHC.Prim
-- it's just easier to get to this way
import Data.Constraint (Constraint)

class All (c :: * -> Constraint) (l :: [*]) where
    allDict :: p1 c -> p2 l -> DList c l

data DList (ctx :: * -> Constraint) (l :: [*]) where
    DCons :: (ctx h, All ctx t) => DList ctx (h ': t)
    DNil  ::                       DList ctx '[]

DList действительно список словарей. DCons захватывает словарь для ограничения, примененного к главному элементу (ctx h), и все словари для остальной части списка (All ctx t). Мы не можем получить словари для хвоста напрямую из конструктора, но можем написать функцию, извлекающую их из словаря для All ctx t.

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy

dtail :: forall ctx h t. DList ctx (h ': t) -> DList ctx t
dtail DCons = allDict (Proxy :: Proxy ctx) (Proxy :: Proxy t)

Пустой список типов тривиально удовлетворяет любому ограничению, применяемому ко всем его элементам.

instance All c '[] where
    allDict _ _ = DNil

Если начало списка удовлетворяет ограничению, а также весь хвост, то все в списке удовлетворяет ограничению.

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

instance (c h, All c t) => All c (h ': t) where
    allDict _ _ = DCons

Теперь мы можем написать ofType, что требует foralls для определения области видимости переменных типа с ScopedTypeVariables.

import Data.Maybe

ofType :: forall a l. (All Typeable l, Typeable a) => HList l -> [a]
ofType l = ofType' (allDict (Proxy :: Proxy Typeable) l) l
  where
    ofType' :: forall l. (All Typeable l) => DList Typeable l -> HList l -> [a]
    ofType' d@DCons (HCons x t) = maybeToList (cast x) ++ ofType' (dtail d) t
    ofType' DNil    HNil        = []

Мы архивируем HList вместе с его словарями с помощью maybeToList . cast и объединяем результаты. Мы можем сделать это явным с помощью RankNTypes.

{-# LANGUAGE RankNTypes #-}

import Data.Monoid (Monoid, (<>), mempty)

zipDHWith :: forall c w l p. (All c l, Monoid w) => (forall a. (c a) => a -> w) -> p c -> HList l -> w
zipDHWith f p l = zipDHWith' (allDict p l) l
  where
    zipDHWith' :: forall l. (All c l) => DList c l -> HList l -> w
    zipDHWith' d@DCons (HCons x t) = f x <> zipDHWith' (dtail d) t
    zipDHWith' DNil    HNil        = mempty

ofType :: (All Typeable l, Typeable a) => HList l -> [a]
ofType = zipDHWith (maybeToList . cast) (Proxy :: Proxy Typeable) 

†ограничения