Обеспечение того типа Haskell А содержит элемент типа B

Question

Давайте посмотрим на следующий код:

transformBi (++"asdasd") [1,2,3,4] 

Очевидно, что этот код ничего не делает, но он по-прежнему отлично компилируется. Я хотел бы создать новую версию transformBi, которая не будет компилироваться, если компилятор может доказать по типам, что это не-op. В идеале, это будет сделано в класс типов под названием Contains, так что тип нового transformBi будет

transformBi :: (Biplate from to, Contains from to) => (to -> to) -> from -> from 

Как мы реализуем Contains?

Я ищу Contains, который может быть автоматически получен, а не для чего-то, что я должен написать для каждого типа алгебраических данных.

Answer 1

Contains может быть пустым классом типа, поскольку он не имеет методов. Вы предоставляете только те экземпляры, которые вам нужны. Например, в этом случае, если у вас есть только

class Contains from to 

instance Contains [a] a 

ваш пример кода не будет компилировать, потому что нет ничего соответствия instance Contains [Int] String.

Если вы планируете широко использовать Contains, вы можете изменить определение на class Biplate from to => Contains from to, а затем вам нужно будет указать ограничение Contains.

Обратите внимание, что если у вас есть большой юниверс вложенных типов, вам может потребоваться написать много экземпляров Contains.

Я бы ожидал, что вы можете просто опустить Biplate экземпляров вместо добавления этого дополнительного класса, однако похоже, что есть довольно широкий instance (Data a, Data b, Uniplate b, Typeable a, Typeable b) => Biplate a b, так что это не будет работать.

Answer 2

Если для типа существует экземпляр Generic, мы можем искать тип его общего представления для определенного поля. Мы хотели бы, чтобы иметь возможность пересекать рекурсивные и взаимно рекурсивных типов, так что нам нужно:

1. Убедитесь, что мы делаем не цикл бесконечно рекурсивных типов. Нам нужно вести учет посещенных типов и останавливаться, когда мы сталкиваемся с ними.

2. Сделать семейный звонок достаточно ленивым, чтобы на самом деле GHC останавливается вычисляет, когда мы этого хотим. Семейства закрытого типа только ленивы по уравнению уравнения сверху вниз (т. Е. Вычисление останавливается при первом согласующем уравнении), поэтому мы используем помощник для рекурсии.

Здесь:

{-# LANGUAGE 
    TypeOperators, 
    TypeFamilies, 
    DataKinds, 
    ConstraintKinds, 
    UndecidableInstances, 
    DeriveGeneric, 
    DeriveDataTypeable 
    #-} 

import Data.Generics.Uniplate.Data 
import GHC.Generics 
import Data.Type.Bool 
import Data.Type.Equality 
import Data.Data 

type family Elem (x :: *) (xs :: [*]) :: Bool where 
    Elem x '[]  = False 
    Elem x (y ': xs) = (x == y) || Elem x xs 

type family LazyRec hasVisited vis t x where 
    LazyRec True vis x y = False 
    LazyRec False vis x x = True 
    LazyRec False vis t x = Contains (t ': vis) (Rep t()) x 

type family Contains (visited :: [*]) (t :: *) (x :: *) :: Bool where 
    Contains vis (K1 i c p) x = LazyRec (Elem c vis) vis c x 
    Contains vis ((:+:) f g p) x = Contains vis (f p) x || Contains vis (g p) x 
    Contains vis ((:*:) f g p) x = Contains vis (f p) x || Contains vis (g p) x 
    Contains vis ((:.:) f g p) x = Contains vis (f (g p)) x 
    Contains vis (M1 i t f p) x = Contains vis (f p) x 
    Contains vis t    x = False 

Теперь мы можем определить стенографии для Biplate, который работает только тогда, когда from возможно содержит to поле:

type family Biplate' from to where 
    Biplate' from to = (Contains '[from] (Rep from()) to ~ True, Biplate from to) 

И вот:

transformBi' :: Biplate' from to => (to -> to) -> from -> from 
transformBi'= transformBi 

-- this one typechecks, but it's a no-op. 
foo :: [Int] 
foo = transformBi (++"foo") ([0..10] :: [Int]) 

-- type error 
foo' :: [Int] 
foo' = transformBi' (++"foo") ([0..10] :: [Int]) 

-- works as intended 
foo'' :: [Int] 
foo'' = transformBi' (+(10::Int)) ([0..10] :: [Int]) 

-- works for recursive/mutually recursive types too 
data Foo = Foo Int Bar deriving (Show, Generic, Typeable, Data) 
data Bar = Nil | Cons() Foo deriving (Show, Generic, Typeable, Data) 

foo''' :: Bar 
foo''' = transformBi' (+(10::Int)) (Cons() (Foo 0 Nil)) 

Некоторые примечания:

• это работает только для Data.Generic.Uniplate.Data. В случае Uniplate.Direct мы можем реализовать пользовательские biplate -s, которые могут или не могут посещать определенные поля, поэтому мы больше не можем рассуждать о том, что не работает, а что нет, что является еще одной причиной, почему это не работает.

• Мы полагаемся на консистенцию GHC и внутренних элементов uniplate, i. е. мы предположим, что uniplate посещает поле to, если Rep содержит соответствующее поле. Это разумное предположение, но может быть нарушено ошибками, находящимися вне нашего контроля. Кроме того, мы должны изменить определение Contains при изменении API представления Generic. С другой стороны, мы не платим штраф за выполнение во время Generic, так как мы проверяем только Rep во время компиляции.