Обеспечение гетерогенного списка содержит один класс типов - PullRequest
Новая
       4

Обеспечение гетерогенного списка содержит один класс типов

0 голосов
/ 01 июня 2018

Я написал свою собственную реализацию гетерогенных списков (сначала я прочитал о гетерогенных списках здесь , и моя реализация очень похожа на их) 

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}

data HList a where
  (:>) :: a -> HList b -> HList (a ': b)
  Nil  :: HList '[]
infixr 6 :>

Это замечательно;однако, как только я обнаружил, что работаю с этими разнородными списками, я часто хотел выразить идею о том, где каждый тип принадлежит определенному классу типов.Мое наивное первое решение здесь - полностью переписать тип данных HList для каждого нового класса типов.Вот для Eq (только для примера; это не единственный класс типов, который меня интересует): 

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}

data EqHList a where
  (:>) :: (Eq a) => a -> EqHList b -> EqHList (a ': b)
  Nil :: EqHList '[]
infixr 6 :>

У этого есть целый ряд проблем.Во-первых, мне нужно переписывать его каждый раз, когда я хочу новый класс типов.Кроме того, функции, которые работают с моими старыми гетерогенными списками, не работают с новыми.

Моим следующим решением было использование пустых классов типов. 

{-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleInstances, FlexibleContexts #-}

data HList a where
  (:>) :: a -> HList b -> HList (a ': b)
  Nil :: HList '[]
infixr 6 :>

class Eqed a

instance Eqed (HList '[])
instance (Eq a, Eqed (HList b)) => Eqed (HList (a ': b))

Здесь экземпляр Eqed является HList, все элементы которого являются экземплярами Eq.Это, конечно, лучше, чем последнее решение, однако я все еще чувствую, что его не хватает.Мне все еще приходится копировать и вставлять кучу кода каждый раз, когда я хочу поговорить о классе другого типа.Я чувствую, что это тип проблемы, который можно решить с помощью программирования на уровне типов.

Есть ли лучший способ?

Ответы [ 2 ]

0 голосов
/ 01 июня 2018

Вы можете использовать ConstraintKinds, чтобы сделать ограничение параметром HList: 

data HList c a where
  (:>) :: (c a) => a -> HList c b -> HList c (a ': b)
  Nil :: HList c '[]

exampleList :: HList Eq '[Int, String, Double]
exampleList
  = (1 :: Int)
  :> ("two" :: String)
  :> (3.0 :: Double)
  :> Nil

Или использовать ExistentialTypes / GADTs и обычный список, если вам нужен только класс типови не стесняйтесь потерять статическую информацию о типах конкретных типов в списке: 

data SomeEq = forall a. Eq a => SomeEq a

data SomeEq where
  SomeEq :: Eq a => a -> SomeEq

exampleList :: [SomeEq]
exampleList =
  [ SomeEq (1 :: Int)
  , SomeEq ("two" :: String)
  , SomeEq (3.0 :: Double)
  ]

Однако это не очень полезно в случае Eq, если только вы не распространяете информацию оНапечатайте равенства, чтобы у вас было что-то полезное, с чем вы хотите сравнить абстрактное переносимое значение.На самом деле, единственное, что вы можете сделать с этим, это сравнить упакованное значение с самим собой.

В зависимости от вашего конкретного приложения могут быть лучшие / более простые варианты.

0 голосов
/ 01 июня 2018

Вы можете обобщить Eqed путем его параметризации (требуется несколько расширений, в сообщениях об ошибках GHC будет указано): 

import Data.Kind (Constraint)

class CMap (c :: * -> Constraint) (xs :: [*])
instance CMap c '[]
instance (c x, CMap c xs) => CMap c (x ': xs)

Однако это не совсем хорошо, потому что CMap c (x ': xs) неподразумевается c x, это только наоборот.Один из способов может состоять в том, чтобы добавить метод, который может использовать эти индивидуальные ограничения, но который кажется сложнымДругой - использовать семейство типов: 

type family CMap (c :: * -> Constraint) (xs :: [*]) :: Constraint where
  CMap c '[] = ()
  CMap c (x ': xs) = (c x, CMap c xs)
...