用泛型删除某些类型的字段-sop

Question

我目前正在为一个涉及从给定数据类型定义派生新的相关数据类型的用例评估Generics.SOP。

首先，我要定义一个表示lambda术语的数据类型的“”版本：

-- The reproducer needs only some of the LANGUAGE pragmas and imports,
-- but it might be convenient for your (or my) solutions
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TemplateHaskell #-}

module SOP where

import Data.SOP.NS
import Generics.SOP
import Generics.SOP.TH
import Data.Kind

newtype Var = V String
  deriving (Eq, Ord, Show)

newtype BindingOcc = B Var
  deriving (Eq, Ord, Show)

data Expr
  = Var Var
  | App Expr Expr
  | Lam BindingOcc Expr

deriveGeneric ''Expr -- Code Expr = '[ '[Var], '[Expr, Expr], '[BindingOcc, Expr]]

要派生出Expr的derive，我必须删除所有的BindingOcc(然后添加一个新的'[Int]替代方案，但一个又一个步骤)。我该怎么做？也许有一种功能

-- Let's be absolutely explicit about it and inline `Code`
-- Also don't want to confuse the type-checker with a type
-- family that removes the field just yet
deleteBindingOcc_SOP :: SOP I '[ '[Var], '[Expr, Expr], '[BindingOcc, Expr]]
                     -> SOP I '[ '[Var], '[Expr, Expr], '[Expr]]
deleteBindingOcc_SOP arg = SOP $ trans_NS Proxy {- will be filled in below -} deleteBindingOcc_NP (unSOP arg)

deleteBindingOcc_NP :: NP I xs -> NP I (WithoutBindingOccs xs)
deleteBindingOcc_NP Nil = Nil
deleteBindingOcc_NP (x :* xs)
  | B _ <- x  = deleteBindingOcc_NP xs
  | otherwise = x :* deleteBindingOcc_NP xs

-- I guess I expected to write the following type family
type family WithoutBindingOcc (xs :: [Type]) :: [Type] where
  WithoutBindingOcc '[]                = '[]
  WithoutBindingOcc (BindingOcc ': xs) = WithoutBindingOcc xs
  WithoutBindingOcc (x          ': xs) = x ': WithoutBindingOcc xs

但是，遗憾的是，这并不是类型检查；首先，我在运行时在xs的定义中匹配deleteBindingOcc_NP的参数多态头，所以我需要一个单例编码/派生一个类型类来定义我的小助手函数deleteBindingOcc_NP。

下面是：

-- Now we know the full type of the proxy, carrying the constraint that `deleteBindingOcc_NP` wants
deleteBindingOcc_SOP arg = SOP $ trans_NS (Proxy :: Proxy MyC) deleteBindingOcc_NP (unSOP arg)

class b ~ WithoutBindingOcc a => MyC a b where -- welp
  deleteBindingOcc_NP :: NP I a -> NP I b
instance MyC '[] '[] where
  deleteBindingOcc_NP Nil = Nil
instance {-# OVERLAPPING #-} MyC a b => MyC (BindingOcc ': a) b where
  deleteBindingOcc_NP (_ :* xs) = deleteBindingOcc_NP xs
instance {-# OVERLAPPABLE #-} MyC a b => MyC (x ': a) (x ': b) where
  deleteBindingOcc_NP (x :* xs) = x :* deleteBindingOcc_NP xs

但是即使这样也不起作用，因为重叠的实例不会进行类型检查：

    • Could not deduce: WithoutBindingOcc (x : a) ~ (x : b)
        arising from the superclasses of an instance declaration
      from the context: MyC a b
        bound by the instance declaration at SOP2.hs:52:31-62
    • In the instance declaration for ‘MyC (x : a) (x : b)’
   |
52 | instance {-# OVERLAPPABLE #-} MyC a b => MyC (x ': a) (x ': b) where
   |                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

考虑一下这一点，这就不足为奇了:不能保证后一种类型的类从未用BindingOcc来实例化它的头x，我们的类型家族应该删除它。所以看来，基于类型的方法不是我想要的。

我的问题是:如何使用给定类型的签名来编写deleteBindingOcc_SOP，使其与不同的、但类似于相关的Code一起工作？

我担心Code表示作为元语言Type构造列表的列表可能不适合实现我想要的结果。不知怎么的，我们不知道所有的Type实际上都是封闭的，不会再被替代了。

Answer 1

也许我们可以依赖于功能依赖关系，而不是使用类型家族来关联原始类型和剥离类型：

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-} -- required by some of the magic below
{-# LANGUAGE TypeApplications #-}

class MyC a b | a -> b where 
  deleteBindingOcc_NP :: NP I a -> NP I b
instance MyC '[] '[] where
  deleteBindingOcc_NP Nil = Nil
instance {-# OVERLAPPING #-} MyC a b => MyC (BindingOcc ': a) b where
  deleteBindingOcc_NP (_ :* xs) = deleteBindingOcc_NP xs
instance {-# OVERLAPPABLE #-} MyC a b => MyC (x ': a) (x ': b) where
  deleteBindingOcc_NP (x :* xs) = x :* deleteBindingOcc_NP xs

这似乎是可行的：

deleteBindingOcc_SOP :: SOP I '[ '[Var], '[Expr, Expr], '[BindingOcc, Expr]]
                     -> SOP I '[ '[Var], '[Expr, Expr], '[Expr]]
deleteBindingOcc_SOP arg = SOP $ trans_NS (Proxy @MyC) deleteBindingOcc_NP (unSOP arg) 

具有辅助MyC'类而不是重叠实例的替代版本：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
import Data.Kind
import GHC.TypeLits
import Data.Type.Equality

class MyC a b | a -> b where 
  deleteBindingOcc_NP :: NP I a -> NP I b
class MyC' (isocc :: Bool)  a b | a -> b where 
  deleteBindingOcc_NP' :: NP I a -> NP I b
instance MyC '[] '[] where
  deleteBindingOcc_NP Nil = Nil
instance MyC' (x == BindingOcc) (x ': xs) ys => MyC (x ': xs) ys where
  deleteBindingOcc_NP = deleteBindingOcc_NP' @(x == BindingOcc)
instance MyC a b => MyC' True (BindingOcc ': a) b where
  deleteBindingOcc_NP' (_ :* xs) = deleteBindingOcc_NP xs
instance MyC a b => MyC' False (x ': a) (x ': b) where
  deleteBindingOcc_NP' (x :* xs) = x :* deleteBindingOcc_NP xs

Answer 2

我不知道你在做什么是不是个好主意..。

但是，抛开所有这些，这里有些东西至少适用于您的简单用例。

type family Equal (a :: k) (b :: k) :: Bool where
  Equal a a = True
  Equal _ _ = False

type family IfThenElse (b :: Bool) (t :: a) (e :: a) where
  IfThenElse True  t _ = t
  IfThenElse False _ e = e

class CanDecide (b :: Bool) where
  ifthenelse :: Proxy b -> ((b ~ True) => r) -> ((b ~ False) => r) -> r

instance CanDecide True  where ifthenelse _ x _ = x
instance CanDecide False where ifthenelse _ _ y = y

class    CanDecide (Equal a BindingOcc) => IsBindingOcc a
instance CanDecide (Equal a BindingOcc) => IsBindingOcc a

type family DeleteBindingOcc (xs :: [Type]) :: [Type] where
  DeleteBindingOcc '[]      = '[]
  DeleteBindingOcc (x : xs) = IfThenElse (Equal x BindingOcc) (DeleteBindingOcc xs) (x : DeleteBindingOcc xs)

class    (All IsBindingOcc xs, DeleteBindingOcc xs ~ ys) => RelDeleteBindingOcc xs ys
instance (All IsBindingOcc xs, DeleteBindingOcc xs ~ ys) => RelDeleteBindingOcc xs ys

deleteBindingOcc_NP :: RelDeleteBindingOcc xs ys => NP f xs -> NP f ys
deleteBindingOcc_NP Nil = Nil
deleteBindingOcc_NP ((x :: f x) :* xs) =
  let
    ys = deleteBindingOcc_NP xs
  in
    ifthenelse (Proxy @(Equal x BindingOcc)) ys (x :* ys)

deleteBindingOcc_SOP :: SOP I '[ '[Var], '[Expr, Expr], '[BindingOcc, Expr]]
                     -> SOP I '[ '[Var], '[Expr, Expr], '[Expr]]
deleteBindingOcc_SOP arg = SOP $ trans_NS (Proxy @RelDeleteBindingOcc) deleteBindingOcc_NP (unSOP arg)

顺便说一句，有一个名为非专利数据外科的漂亮库(不幸的是，我从未使用过它)，它声称自己擅长这类事情。