Обеспечение того, чтобы тип A haskell содержал член типа B

Question

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

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

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

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

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

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

Answer 1

Если есть 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- которые могут посещать или не посещать определенные поля, поэтому мы больше не можем рассуждать о том, что запрещено, а что нет, что является еще одной причиной, по которой это не работает.

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

Answer 2

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 так что это не сработает.