如何正确地包装归纳数据类型索引的数据类型？

Question

我正在尝试将列表的单例版本简化。我很难解构它。这是一个最小的实现：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ExplicitForAll #-}

module InductiveWrapper where

import Data.Kind (Type)
import Data.Proxy (Proxy)

import GHC.Prim (coerce)

data List a = Nil | Cons a (List a)

data SList :: [ k ] -> Type where
  SNil  ::                        SList '[]
  SCons :: Proxy k -> SList ks -> SList (k ': ks)

newtype Set a = S [ a ]

data SSet :: Set k -> Type where
  SS :: SList xs -> SSet ('S xs)

type family Add (el :: k) (set :: Set k) :: Set k where
  Add el ('S xs) = 'S (el ': xs)

uncons :: forall k (el :: k) (set :: Set k)
        . SSet (Add el set) -> (Proxy el, SSet set)
uncons (SS (x `SCons` xs)) = (x, SS xs)

以下是错误的相关位：

Could not deduce: set ~ 'S ks
      from the context: Add el set ~ 'S xs
        bound by a pattern with constructor:
                   SS :: forall k (xs :: [k]). SList xs -> SSet ('S xs),
                 in an equation for ‘uncons’
[...]
 or from: xs ~ (k1 : ks)
        bound by a pattern with constructor:
                   SCons :: forall k1 (k2 :: k1) (ks :: [k1]).
                            Proxy k2 -> SList ks -> SList (k2 : ks),
[...]
• Relevant bindings include
        xs :: SList ks (bound at InductiveWrapper.hs:37:29)
        x :: Proxy k1 (bound at InductiveWrapper.hs:37:19)
        xs' :: SList xs (bound at InductiveWrapper.hs:37:14)
        s :: SSet (Add el set) (bound at InductiveWrapper.hs:37:8)

据我所知，问题是Add el set被卡住了，因为类型检查器不了解可以构造set的唯一方法是使用'S。

我如何解开它或通过其他方式解决此问题？除了使用type代替newtype。我这样做的全部原因是完全隐藏了[ k ]和SList的使用。

Answer 1

类型族是非单射的，从技术上讲，这意味着您不能从结果到参数，从右到左。除了没有GHC 8.0引入了TypeFamilyDependencies，可让您指定类型族的插入性，如下所示：

type family Add (el :: k) (set :: Set k) = (set' :: Set k) | set' -> el set where
  Add el ('S xs) = 'S (el ': xs)

但是，由于某些原因，我尚不完全了解，这在您的情况下仍然不起作用，导致了同样的问题。我怀疑这可能与问题清单是双重包装的事实有关，不确定。

但是我确实有另一个解决方法：您可以放弃整个内射性问题，并以其他方式指定类型族-从列表到元组。除非您需要two类型族-一个用于头部，一个用于尾巴：

type family Head set where Head ('S (el ': xs)) = el
type family Tail set where Tail ('S (el ': xs)) = 'S xs

uncons :: SSet set -> (Proxy (Head set), SSet (Tail set))
uncons (SS (x `SCons` xs)) = (x, SS xs)

但是这对我来说似乎有点过分设计。如果您只需要取消约束这些类​​型集，那么我会推荐一个好的ol'type类，它具有将类型和值包装在一起的无与伦比的优势，因此您不必为了手动匹配它们而跳了圈：

class Uncons set res | set -> res  where
    uncons :: SSet set -> res

instance Uncons ('S (el ': xs)) (Proxy el, SSet ('S xs)) where
    uncons (SS (x `SCons` xs)) = (x, SS xs)