haskell - 如何编写函数将泛型类型转换为标签形类型以与 DSum 一起使用？

Question

如何实现这个toDSum函数？我已经成功编译了基本情况，但我不知道如何在递归调用中携带所有类型信息。在尝试递归之前，我是否必须从类型中删除 Code ？

(这是 How can I write this GEq instance? 的后续内容)

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Foo where

import Data.Dependent.Sum
import Data.GADT.Compare
import Data.Proxy
import Generics.SOP
import qualified GHC.Generics as GHC

type GTag t = GTag_ (Code t)
newtype GTag_ t (as :: [*]) = GTag (NS ((:~:) as) t)

instance GEq (GTag_ t) where
  geq (GTag (Z Refl)) (GTag (Z Refl)) = Just Refl
  geq (GTag (S x))    (GTag (S y))    = GTag x `geq` GTag y
  geq _               _               = Nothing

toDSum :: forall t . Generic t => t -> DSum (GTag t) (NP I)
toDSum = foo . unSOP . from
  where
    foo :: ()
        => NS (NP I) (Code t)
        -> DSum (GTag t) (NP I)
    foo = bar (Proxy :: Proxy t)

    bar :: forall t1 . ()
        => Proxy t1 -> NS (NP I) (Code t1)
        -> DSum (GTag t1) (NP I)
    bar _ (Z x) = GTag (Z Refl) :=> x
    bar _ (S x) = undefined

Answer 1

此代码的一个版本位于我的 other 中答案，但类型略有不同，这实际上简化了代码。

正如您在实例 GEq (GTag_t) 中看到的那样，当您想要在 NS 或 NP 上编写归纳函数时，您需要为了保持索引参数化——你会在“依赖”编程中看到这种一般模式(包括真正的依赖编程和在 Haskell 中伪造的编程)。

这正是 bar 的问题:

forall t1 . () => Proxy t1 -> NS (NP I) (Code t1) -> DSum (GTag t1) (NP I)
                                        ^^^^^^^^^

这样的函数不可能是递归的 - 只是因为如果S rep::NS (NP I) (Code t1)，那么情况不一定如此(事实上，它这里的情况从来都不是这样)，对于某些t2，rep::NS (NP I) (Code t2) - 即使这个事实是确实，你很难让编译器相信这一点。

您必须在索引中将此函数(重命名为 toTagValG)参数化:

type GTagVal_ t = DSum (GTag_ t) (NP I)
type GTagVal t = DSum (GTag t) (NP I)

toTagValG :: NS f xss -> DSum (GTag_ xss) f 
toTagValG (Z rep) = GTag (Z Refl) :=> rep 
toTagValG (S rep) = case toTagValG rep of GTag tg :=> args -> GTag (S tg) :=> args

然后，当您使用 to 或 from 时，xss 会使用 Code t 实例化，因为 from::a -> Rep a 和 Rep a = SOP I(代码 a):

toTagVal :: Generic a => a -> GTagVal a
toTagVal = toTagValG . unSOP . from 

请注意，此类型是推断出来的(如果您关闭 MonomorphismRestriction)

另一个方向更简单:

fromTagVal :: Generic a => GTagVal a -> a 
fromTagVal = to . SOP . (\(GTag tg :=> args) -> hmap (\Refl -> args) tg) 

尽管您也可以通过归纳在 lambda 中编写函数:

fromTagValG :: DSum (GTag_ xss) f -> NS f xss 
fromTagValG (GTag (Z Refl) :=> rep) = Z rep 
fromTagValG (GTag (S tg) :=> args) = S $ fromTagValG $ GTag tg :=> args 

请注意，您可以为此函数分配一个非常通用的类型，并且toTagValG - 事实上，它根本没有提及NP I。您还应该能够让自己相信这些函数互为逆函数，从而见证 NS f xss 和 DSum (GTag_ xss) f 之间的同构。