我如何编写函数将泛型类型转换为与DSum一起使用的标记形状类型？ [英] How can I write function to convert generic type to Tag-shaped type for use with DSum?

问题描述

如何实现这个 toDSum 函数？我已经设法得到基本情况进行编译，但我不知道如何通过递归调用来承载所有类型信息。在尝试递归之前，是否必须从类型中去掉 Code >？

（这是我该如何编写这个GEq实例？）

  { - ＃LANGUAGE GADTs＃ - } 
 { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃ LANGUAGE TypeOperators＃ - } 
 { - ＃LANGUAGE KindSignatures＃ - } 
 { - ＃LANGUAGE RankNTypes＃ - } 
 { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 
 module Foo其中
 
导入Data.Dependent.Sum 
导入Data.GADT.Compare 
导入Data.Proxy 
导入Generics.SOP 
导入限定的GHC。泛型为GHC 
 
类型GTag t = GTag_（代码t）
新类型GTag_ t（as :: [*]）= GTag（NS（（：〜:) as）t）
 
实例GEq（GTag_t）其中
 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。通用t => t  - > DSum（GTag t）（NP I）
 toDSum = foo。 unSOP。 from 
 where 
 foo ::（）
 => NS（NP I）（代码t）
  - > DSum（GTag t）（NP I）
 foo = bar（Proxy :: Proxy t）
 
 bar :: forall t1。 （）
 =>代理t1  - > NS（NP I）（代码t1）
  - > DSum（GTag t1）（NP I）
 bar _（Z x）= GTag（Z Refl）：=> x 
 bar _（S x）=未定义
  

解决方案

<这段代码的一个版本在我的 other 答案，但类型略有不同，这实际上简化了代码。

正如你在实例GEq（GTag_t）中看到的那样，当你想在 NS> >上编写归纳函数时，或 NP ，你需要保持索引参数化 - 你会看到这个通用模式与'依赖'编程有很大关系（都是真正的依赖编程，并在Haskell中伪造）。

这恰恰是 bar 的问题：

  forall t1。 （）=>代理t1  - > NS（NP I）（代码t1） - > DSum（GTag t1）（NP I）
 ^^^^^^^^^ 
  

这样的函数没有办法递归 - 仅仅因为如果 S rep :: NS（NP I）（Code t1），那么它不一定是这种情况（实际上，这里从来就不是这种情况）：对于某些 t2 rep :: NS（NP I）（代码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代表GTag tg：=> args  - > GTag（S tg）：=> args 
  

然后 xss 被实例化为<$从使用至或时，c $ c> Code t $ c> from :: a - > Rep a 和 Rep a = SOP I（Code a）：

  toTagVal :: Generic a => a  - > GTagVal 
 toTagVal = toTagValG。 unSOP。从
  

注意这种类型是推断的（如果关闭MonomorphismRestriction）

另一个方向更简单：

  fromTagVal :: Generic a => GTagVal a  - >从TavVal =到
。 SOP。 （\（GTag tg：=> args） - > hmap（\Refl-> args）tg）
  

尽管您可以在函数中使用导入函数来编写函数：

  fromTagValG :: DSum（GTag_ xss）f  - > （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 。

How can I implement this toDSum function? I've managed to get the base case to compile, but I don't know how to carry all the type information across a recursive call. Do I have to strip off the Code from the type before trying to recurse?

(this is a followup to 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

解决方案

A version of this code was in my other answer, but the types are slightly different, which actually simplifies the code.

As you have seen with instance GEq (GTag_ t), when you want to write inductive functions on NS or NP, you need to keep the index parametric - you will see this general pattern quite a bit with 'dependant' programming (both real dependant programming and faking it in Haskell).

This is precisely the issue with bar:

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

There is no way for such a function to be recursive - simply because if S rep :: NS (NP I) (Code t1), then it is not necessarily the case (indeed, it is never the case here) that rep :: NS (NP I) (Code t2) for some t2 - and even if this fact were true, you would struggle to convince the compiler of it.

You must make this function (renaming to toTagValG) parametric in the index:

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

Then xss is instantiated with Code t when you use to or from, since from :: a -> Rep a and Rep a = SOP I (Code a):

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

Note this type is inferred (if you turn off the MonomorphismRestriction)

The other direction is even simpler:

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

Although you can write the function in the lambda with induction as well:

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 

Note that you can assign a very general type to this function, and toTagValG - indeed, it does not mention NP I at all. You should also be able to convince yourself that these functions are each others inverses, and so witness an isomorphism between NS f xss and DSum (GTag_ xss) f.

这篇关于我如何编写函数将泛型类型转换为与DSum一起使用的标记形状类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！