Проверка, содержит ли один список уровня типа другой

Можно ли написать функцию уровня типа, которая возвращаетTrue если один список уровня типа содержит другой список уровня типа?

Вот моя попытка:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module TypePlayground where

import Data.Type.Bool

type family InList (x :: *) (xs :: [*]) where
    InList x '[] = 'False
    InList x (x ': xs) = 'True
    InList x (a ': xs) = InList x xs
type family ListContainsList (xs :: [*]) (ys :: [*]) where
    ListContainsList xs (y ': ys) = InList y xs && ListContainsList xs ys
    ListContainsList xs '[] = 'True

Это работает для простых случаев:

data A
data B
data C

test1 :: (ListContainsList '[A, B, C] '[C, A] ~ 'True) => ()
test1 = ()
-- compiles.
test2 :: (ListContainsList '[A, B, C] '[B, C, A] ~ 'True) => ()
test2 = ()
-- compiles.
test3 :: (ListContainsList (A ': B ': '[C]) (B ': A ': '[C]) ~ 'True) => ()
test3 = ()
-- compiles.
test4 :: (ListContainsList '[A, C] '[B, C, A] ~ 'True) => ()
test4 = ()
-- Couldn't match type ‘'False’ with ‘'True’

Но как насчет таких случаев?

test5 :: (ListContainsList (A ': B ': a) a ~ 'True) => ()
test5 = ()
-- Should compile, but fails:
-- Could not deduce (ListContainsList (A : B : a0) a0 ~ 'True)
-- from the context (ListContainsList (A : B : a) a ~ 'True)
 gallais06 июл. 2016 г., 09:19
У меня была похожая проблема, хотя немного проще (проверка,h являетсяg ++ g' для некоторыхg') и это заняло у меня очень много времени, прежде чемзаставить что-то работать даже с открытыми типами. Использование тех же приемов (и языковых расширений!) Может привести вас в правильном направлении.
 Hoff06 июл. 2016 г., 11:29
Хм, я не думаю, что средство проверки типа haskell может делать такие вещи, даже если это было бы совершенно потрясающе ...
 jkeuhlen05 июл. 2016 г., 23:28
У меня нет времени выкинуть и проверить полный ответ, но как насчет использованияData.Type.List и видеть, является ли объединение первого списка со вторым таким же, как первый или второй список (один содержит другой).

Ответы на вопрос(2)

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

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

data Elem xs x where
    Here :: Elem (x ': xs) x
    There :: Elem xs x -> Elem (y ': xs) x

Elem структурирован как натуральное число (сравнитеThere (There Here) сS (S Z)) но с большим количеством типов. Чтобы доказать, что элемент находится в списке, вы указываете его индекс.

data All f xs where
    Nil :: All f '[]
    Cons :: f x -> All f xs -> All f (x ': xs)

All является доказательством того, что данный предикат применяется к каждому элементу списка. Он структурирован как список доказательствf.

Теперь тип доказательств того, что список является подмножеством другого списка, легко записать с помощью этих частей механизма.

type IsSubset xs ys = All (Elem ys) xs

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

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

 Roman Cheplyaka06 июл. 2016 г., 14:03
Классная напыщенная речь, но я сомневаюсь, что это помогает ОП вообще.
 WorldSEnder03 авг. 2018 г., 22:31
Как бы вы пошли о доказыванииNotElem? Мой лучший подход будетdata Bottom, type NotElem xs x = Elem xs x -> Bottom в паре сnotInEmpty :: NotElem '[] x а такжеnotHere :: (x :~: y -> Bottom) -> NotElem xs x -> NotElem (y : xs) x который должен быть реализован довольно легко. У вас есть идеи получше?
 Benjamin Hodgson06 авг. 2018 г., 10:12
@WorldSEnder Да, это работает. КонструктивноNotElem xs x является доказательством того, что вxs где вы можете найтиx, Альтернативой было бы дать список доказательств того, что каждый элемент вxs не являетсяxт.е.All (Not . (:~: x)) xs, В качестве упражнения вы можете попытаться засвидетельствовать изоморфизм между этими формами (вашиnotInEmpty а такжеnotHere функции демонстрируют одно направление)
 Blaisorblade06 июл. 2016 г., 14:56
Увидев эту модель в Агде, я согласен с предложением. Это делаетне решить проблему самостоятельно. Далее нужна лемма о том, что любой список является подсписком сам по себе,reflSubset :: (xs :: [*]) -> IsSubset xs xsи вам нужно доказать это по индукции; Я подозреваю, что это легче написать с помощью этой кодировки (где вы можете вернутьIsSubset), чем использовать версию ОП - что быreflSubset вернуться туда? Может быть, доказательство равенства, но это громоздко. Подпись я написалreflSubset требует зависимых типов, но я подозреваю, что синглтоны позволяют имитировать это.
 nicolas06 июл. 2016 г., 16:52
спасибо за информированный, пусть и самоуверенный, совет
Решение Вопроса

Проблема в том, что вы определили свое семейство типов подмножеств по индукции в структуру содержащегося списка, но вы передаете полностью полиморфный (неизвестный) список, структура которого является загадкой для GHC. Вы можете подумать, что GHC сможет использовать индукцию в любом случае, но вы ошибаетесь. В частности, как и каждыйтип имеет неопределенныйценноститак что каждыйДобрый "застрял"типы, Примечательный пример, который GHC использует внутри страны и экспортирует через (IIRC)GHC.Exts:

{-# LANGUAGE TypeFamilies, PolyKinds #-}

type family Any :: k

Any тип семьи вкаждый Добрый. Таким образом, вы могли бы иметь список уровня типаInt ': Char ': Any, гдеAny используется в натуре[*], Но нет никакого способа деконструироватьAny в': или же[]; у него нет такой разумной формы. С типом семьи какAny существует, GHC не может безопасно использовать индукцию для типов, как вы хотите.

Если вы хотите, чтобы индукция правильно работала над списками типов, вы действительнонеобходимость использовать синглтоны или аналогичные, как предлагает Бенджамин Ходжсон. Вместо того, чтобы передавать только список на уровне типов, вам нужно также передать GADT, подтверждающий, что список на уровне типов построен правильно. Рекурсивное разрушение GADT выполняет индукцию по списку уровня типов.

Те же самые ограничения существуют и для натуральных чисел уровня типа.

data Nat = Z | S Nat
type family (x :: Nat) :+ (y :: Nat) :: Nat where
   'Z :+ y = y
   ('S x) :+ y = 'S (x :+ y)

data Natty (n :: Nat) where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

Вы можете доказать

associative :: p1 x -> p2 y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))

но вы не можете, потому что это требует индукции наx а такжеy, Вы можете, однако, доказать

associative :: Natty x -> Natty y -> p3 z -> ((x :+ y) :+ z) :~: (x :+ (y :+ z))

без проблем.

 Blaisorblade11 июл. 2016 г., 20:09
Чтоp1, p2 а такжеp3?
 dfeuer11 июл. 2016 г., 21:07
@Blaisorblade, они (полиморфные) прокси.
 Benjamin Hodgson12 июл. 2016 г., 14:48
@SergeyMitskevich Если вы новичок в зависимых типах, я бы не советовал использовать Haskell для обучения. Хаскель не является языком с зависимой типизацией; трюки, как синглтоны, просто взломатьмоделировать зависимые типы. Я бы посоветовал сначала выбрать реальную систему с зависимой типизацией, а затем узнать кодировки на Haskell, как только вы поймете концепцию.Сила Пи мое личное любимое вступление
 Sergey Mitskevich12 июл. 2016 г., 14:32
Большое спасибо за ваш ответ (также ответ Бенджамина был очень полезным)! Я новичок в программировании с зависимой типизацией, и определенно кажется, что мне нужно потратить некоторое время на чтение статей, связанных с одиночками, чтобы глубже понять, как решать такие проблемы.
 dfeuer12 июл. 2016 г., 20:03
@SergeyMitskevich, я второй совет Бенджамина Ходжсона, что вы должны выучить хотя бы немного зависимый типизированный язык, чтобы лучше понять эти вещи. Изучение их в Haskell похоже на изучение структур данных в первый раз в C.

Ваш ответ на вопрос