Ограничение на транзитивных дочерних элементах ADT

Question

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

data A = A1 B | A2 C D 
newtype B = B String 
newtype C = C String 
newtype D = D Int 

Я хочу, чтобы иметь возможность определить HasString предикат и функцию getString так:

getString :: (HasString x) => x -> String 

таким образом, что HasString выполняется для A1, B, и C, но не для D.

Стандартный способ сделать такого рода вещи только с ручным обходом:

class GetString t where 
    getString :: t -> String 

instance GetString B where 
    getString (B s) = s 

-- .... instances for A, C 

При написании это, мы в основном создали доказательство того, что каждый A транзитивно содержит String.

Теперь, я хочу сделать это с помощью универсального оборудования, поэтому я могу заставить его работать с типами данных, отличными от A. И мне все равно, кроме getString.

В настоящее время я могу построить предикат уровня уровня, который указывает, транзитный ли тип данных содержит String. Я даже могу построить его с помощью универсального доказательства машины:

type family Or a b where 
    Or True a = True 
    Or a True = True 
    Or a b = False 

type family And a b where 
    And True True = True 
    And a b = False 

type family BaseHasString f where 
    BaseHasString B = True 
    BaseHasString C = True 
    BaseHasString x = False 

type family Has f t where 
    Has f A = Or (f A) (And (Has f B) (Or (Has f C) (Has f D))) 
    Has f x = f x 

type HasString t :: Constraint = (Has BaseHasString t ~ True) 

(. Я должен также быть в состоянии обобщить эту далее с помощью GHC Generics)

Однако теперь, когда у меня есть HasString предикат, я не могу выяснить, как на самом деле использовать его.

Итак, как я могу написать свою функцию getString?

Answer 1

Я пошел в церковь и молился Церкви. И вот, я видел прекрасное видение. Мне открылись платонические формы сумм и типов продуктов. И я увидел, что это хорошо.

Все приведенные примеры являются простыми старыми типами сумм в натуральном выражении *. Теперь Either и (,) являются простейшими суммами и типами продуктов, соответственно, и не следует удивляться тому, что их можно использовать для моделирования всех других сумм и видов продукции в натуральной форме *. Посмотрите - вот ваши примеры, по модулю обертывание и разворачивание:

type A = Either B (C, D) 
type B = String 
type C = String 
type D = Int 

Вы можете сделать большие примеры, вкладывая в Either сек и кортежи:

data IntOrBoolOrChar = Int Int | Bool Bool | Char Char 
type IntOrBoolOrChar = Either Int (Either Bool Char) 

data IntAndBoolAndChar = IBC Int Bool Char 
type IntAndBoolAndChar = (Int, (Bool, Char)) 

Так что, если вы счастливы построить свой типы полностью из Either и (,), мы можем запрограммировать в общих чертах эти два строительных блока.

instance HasString String where 
    getString = id 

instance (HasString a, HasString b) => HasString (Either a b) where 
    getString (Left x) = getString x 
    getString (Right y) = getString y 

Трудный вариант - это кортеж. Идея состоит в том, что если мы сможем найти строку в левом компоненте кортежа (т. Е. HasString a), то мы вернем ее.В противном случае мы рассмотрим правильный компонент. Мы хотели бы написать так:

instance HasString a => HasString (a, b) where 
    getString = getString . fst 
instance HasString b => HasString (a, b) where 
    getString = getString . snd 

Haskell отклоняет эти объявления, потому что экземпляры являются дубликатами. При разрядке ограничения, такого как HasString (a, b), решатель выбирает наиболее конкретный экземпляр, который он может найти для этой главы, и пытается разрешить ограничения экземпляра, но не отбрасывает, если он не может этого сделать.

Спецификация, изложенная выше, является невыразимой в ванильном Haskell. Но есть well-known trick с использованием семейств типов, которые могут помочь нам здесь. Идея состоит в том, чтобы использовать результат семейства типов, чтобы рассказать нам, какую половину кортежа мы можем найти, чтобы найти String дюйма. Это, оказывается, является одним из немногих случаев, когда булевы типа на самом деле полезны.

Итак, когда мы можем найти String в виде?

-- with And and Or being the usual Boolean type families 
type family HasString' a where 
    HasString' String = True 
    HasString' (a, b) = Or (HasString' a) (HasString' b) 
    HasString' (Either a b) = And (HasString' a) (HasString' b) 
    HasString' _ = False 

Как указано на the wiki page I linked above, трюк заключается в добавлении нового класса с дополнительным параметром для результата HasString', который используется для отправки к нужному экземпляру. Вот почему имеет смысл использовать Booleans здесь: я выбор между двумя вариантами. Если бы у меня было три варианта выбора, я бы использовал трехзначный тип. Don't use Booleans to represent propositions.

data Proxy a = Proxy 

class HasStringTup inLeft a b where 
    getStringTup :: Proxy inLeft -> (a, b) -> String 

instance HasStringTup (HasString' a) a b => HasString (a,b) where 
    getString = getStringTup (Proxy :: Proxy (HasString' a)) 

-- HasString' was True for a, so we can get a string from it 
instance HasString a => HasStringTup True a b where 
    getStringTup _ = getString . fst 

-- HasString' was False for a, so look at b 
instance HasString b => HasStringTup False a b where 
    getStringTup _ = getString . snd 

Итак, да. Это большой взлом, и, вероятно, он не стоит сложностей. Особенно неприятно писать обход дважды, как класс и как семейство типов. Чтобы обойти нехватку Haskell в обратном направлении, нам пришлось вручную смотреть в будущее. Ну, он все еще работает:

ghci> getString ('b', (Right "foo" :: Either String String, 3)) 
"foo" 
ghci> getString ("foo", "bar") 
"foo" 

---

Oh! Кстати. Если вы хотите использовать свои собственные типы, а не выражать все как кортежи и Either s, вы все равно можете генерировать общее программирование, преобразовывая их в общее представление и из него. На это накладные расходы, но это расходы, которые вы платите.

Что-то вроде этого:

Вы можете использовать шаблон Haskell писать такого рода случаях для вас. Это более или менее дизайн большинства общих библиотек программирования, таких как GHC.Generics. В основном они имеют более сложный тип представления.