检查一个类型级别列表是否包含另一个 [英] Checking if one type-level list contains another

问题描述

如果一个类型级别列表包含另一个类型级别列表，那么是否可以编写一个返回 True 的类型级别函数？

这是我的尝试：

  { - ＃LANGUAGE TypeOperators＃ - } 
 { - ＃ ＃语言DataKinds＃ - } 
 { - ＃LANGUAGE TypeFamilies＃ - } 
 { - ＃LANGUAGE UndecidableInstances＃ - } 
 
 module TypePlayground其中
 
导入Data.Type.Bool 
 
类型系列InList（x :: *）（xs :: [*]）其中
 InList x'[] ='False 
 InList x x'：xs）='True 
 InList x（a'：xs）= InList x xs 
类型系列ListContainsList（xs :: [*]）（ys :: [*]）其中
 ListContainsList xs（y'：ys）= InList y xs&& ListContainsList xs ys 
 ListContainsList xs'[] ='True 
  

它适用于简单情况：

 数据A 
数据B 
数据C 
 
 test1 ::（ ListContainsList'[A，B，C]'[C，A]〜'True）=> （）
 test1 =（）
  - 编译。 
 test2 ::（ListContainsList'[A，B，C]'[B，C，A]〜'True）=> （）
 test2 =（）
  - 编译。 （B'：A'：'[C]）〜'True）=> （）
 test3 =（）
  - 编译。 
 test4 ::（ListContainsList'[A，C]'[B，C，A]〜'True）=> （）
 test4 =（）
  - 无法将类型''False'与''''匹配
  

但这样的情况怎么样？

  test5 ::（ListContainsList（A'：B '：a）a〜'True）=> （）
 test5 =（）
  - 应该编译，但失败：
  - 无法推断（ListContainsList（A：B：a0）a0〜'True）
  -  - 从上下文（ListContainsList（A：B：a）a〜'True）
  

解决方案

麻烦的是，你通过归纳所包含列表的结构来定义你的子集类型族，但是你正在传递一个完全多态（未知）列表，其结构对GHC来说是一个谜。无论如何，你可能会认为GHC能够使用归纳，但你会错的。特别是，正如每个类型具有未定义的值，所以每个类都有卡住类型。一个值得注意的例子，GHC内部使用和通过（IIRC）出口 GHC.Exts ：

  { - ＃LANGUAGE TypeFamilies，PolyKinds＃ - } 
 
类型系列任何:: k 
  

任何类型系列都在每个类型中。所以你可以有一个类型级的列表 Int'：Char'：任何，其中任何 code> [*] 。但是无法将 Any 解构成'：或 [] ;它没有任何这种明智的形式。由于像 Any 这样的类型系列存在，GHC无法安全地按照您希望的方式使用类型归纳。

如果您想要归纳可以在类型列表中正常工作，你真的需要来使用单身人士或类似的本杰明霍奇森建议。您不需要传递类型级别列表，您还需要传递一个GADT，以证明类型级别列表已正确构建。递归地破坏GADT会在类型级别列表中进行归纳。

类型级自然数的限制也是一样。

 数据Nat = Z | S Nat 
 type family（x :: Nat）：+（y :: Nat）:: Nat where 
'Z：+ y = y 
（'S x）：+ y = 'S（x：+ y）
 
数据Natty（n :: Nat）其中
 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））
  

没有问题。

Is it possible to write a type-level function that returns True if one type-level list contains another type-level list?

Here is my attempt:

{-# 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

It works for simple cases:

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’

But what about cases like this?

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)

解决方案

The trouble is that you've defined your subset type family by induction on the structure of the contained list, but you're passing in a totally polymorphic (unknown) list whose structure is a mystery to GHC. You might think that GHC would be able to use induction anyway, but you'd be wrong. In particular, just as every type has undefined values, so every kind has "stuck" types. A notable example, which GHC uses internally and exports through (IIRC) GHC.Exts:

{-# LANGUAGE TypeFamilies, PolyKinds #-}

type family Any :: k

The Any type family is in every kind. So you could have a type-level list Int ': Char ': Any, where Any is used at kind [*]. But there's no way to deconstruct the Any into ': or []; it doesn't have any such sensible form. Since type families like Any exist, GHC cannot safely use induction on types the way you wish.

If you want induction to work properly over type lists, you really need to use singletons or similar as Benjamin Hodgson suggests. Rather than passing just the type-level list, you need to pass also a GADT giving evidence that the type-level list is constructed properly. Recursively destructing the GADT performs induction over the type-level list.

The same sorts of limitations hold for type-level natural numbers.

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)

You might wish to prove

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

but you can't, because this requires induction on x and y. You can, however, prove

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

with no trouble.

这篇关于检查一个类型级别列表是否包含另一个的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！