ジェネリック型をタグ型に変換して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の回答であったが、種類が若干異なります。

あなたがNSまたはNPに誘導機能を書きたいinstance GEq (GTag_ t)、と見てきたように、あなたは、インデックス、パラメトリックを維持する必要があります - あなたは、この一般的なパターンに「依存」プログラミングとかなり表示されます（両方の本当の依存プログラミングそれをHaskellで偽造する）。

これは正確にbarの問題です：

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

、このような関数は再帰的であるために方法はありません - S rep :: NS (NP I) (Code t1)場合、それは必ずしもそうではありません（実際、それは決してありませんという理由だけでこの場合rep :: NS (NP I) (Code t2)の場合は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 

xssあなたがtoやfromを使用する場合from :: a -> Rep aとRep a = SOP I (Code a)以来、Code tでインスタンス化されています

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) 

あなたにも誘導とラムダ関数を書くことができますが：あなたは、この機能に非常に一般的なタイプを割り当てることができます

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の同型写像を目撃してください。

Answer 2

これはすでに回答済みですが、私は数時間かけて作業してから自分で追加します。

短いと甘い

toDSum :: Generic t => t -> DSum (GTag t) (NP I) 
toDSum = foo (\f b -> GTag f :=> b) . unSOP . from 
    where 
    foo :: (forall a . (NS ((:~:) a) xs) -> NP I a -> r) 
     -> NS (NP I) xs 
     -> r 
    foo k (Z x) =  (k . Z) Refl x 
    foo k (S w) = foo (k . S)  w