Построение конкретных типов для моделей с GADT

Question

Вдохновением для этого является создание списка значений, которые являются экземплярами Show. Я нашел следующий фрагмент, который использует GADT для создания конкретного типа Showable.

data Showable where Showable :: Show a => a -> Showable 

instance Show Showable where 
    show (Showable x) = show x 

list :: [Showable] 
list = [Showable 4, Showable "hello", Showable 'a'] 

Затем я попытался сделать Showable более общим путем создания типа, которые могли бы сделать какой-либо конкретный класс типов.

data Concrete a where Concrete :: a b => b -> Concrete a 

instance Show (Concrete Show) where 
    show (Concrete x) = show x 

list :: [Concrete Show] 
list = [Concrete 4, Concrete "hello", Concrete 'a'] 

Это работает с ConstraintKinds и расширениями FlexibleInstances языка, но для того, чтобы использовать Concrete сделать конкретные типы для других классов типов, каждый из которых требует нового экземпляра.

Есть ли способ создать что-то похожее на Concrete так, что, например, Concrete Show является автоматически экземпляром Show?

Answer 1

Невозможно. Рассмотрим это:

instance Monoid (Concrete Monoid) where 
    mappend (Concrete x) (Concrete y) = Concrete (mappend x y) -- type error! 

Это ошибка типа, поскольку x и y поступают из двух различных экзистенциальных количественными. Нет гарантии, что x и y могут быть добавлены вместе.

Иными словами, [Concrete [1,2], Concrete ["hello"]] имеет тип [Concrete Monoid], но не может быть суммирован (mconcat).

---

Это точно та же проблема, для которой, в ООП, следующий базовый класс/интерфейс не работает:

interface Vector { 
    Vector scale(double x); 
    Vector add(Vector v); 
} 
class Vec2D implements Vector { ... } 
class Vec3D implements Vector { ... } 

Интерфейс предполагает, что 2D вектор addable в любой другой вектор, включая трехмерный, что не имеет смысла. Для решения ООП см. F-bounded quantification и связанной с ним популяризации curiously recurring template pattern.

В Haskell нам часто не нужны такие методы, поскольку нет подтипирования, поэтому два типа, например, классов типа Vector, уже не смешиваются.

class Vector a where 
    scale :: Double -> a -> a 
    add :: a -> a -> a 
instance Vector (Vec2D) where ... 
instance Vector (Vec3D) where ...