如何編寫函數將泛型類型轉換爲與DSum一起使用的標記形狀類型？

我該如何實現這個toDSum函數？我已經設法得到基本情況進行編譯，但我不知道如何通過遞歸調用來承載所有類型信息。在嘗試遞歸之前，我是否必須從類型中去掉Code？如何編寫函數將泛型類型轉換爲與DSum一起使用的標記形狀類型？

（這是一個後續到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

來源

2016-11-20 ajp

你可能會更好過避免'Code'只要有可能。在上下文中，它是一個代碼，還是可以讓它完全呈多態？ – dfeuer

我認爲這是必要的，因爲'GTag t'適合'DSum'，但'GTag_ t'（沒有添加「Code」）不適用。但我可能是錯的。對於完整的上下文，我正在處理這個文件https://github.com/anderspapto/reflex-sumtype-render/blob/master/src/ReflexHelpers.hs，這是謎題的最後一個缺失部分。 – ajp

這個代碼的一個版本是在我other答案，但種類略有不同，這實際上簡化了代碼。

正如你所用instance 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)，那麼它是不是一定的情況下（事實上，這是從來沒有的這裏的情況）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與Code t當您使用to或from，因爲from :: a -> Rep a和Rep a = SOP I (Code 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)

雖然你可以寫在感應拉姆達的功能以及：

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之間的同構。

來源

2016-11-21 05:44:46 user2407038

謝謝！儘管我自己痛苦地解決了這個問題後，看到一個答案，我只是有點難過。我一定會閱讀你的評論，雖然 – ajp

雖然這已經回答了，但是我會自己添加自己的，因爲我花了幾個小時來完成它。

短暫的甜蜜

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

來源

2016-11-21 06:26:05 ajp

的確，我通常稱之爲'case_'的這個函數'foo'基本上說'NS f xs'和exists x是一樣的。（InList x xs，fx）' - 因爲NS（（：〜:) a）xs'是一個指向'xs'的索引，並且證明'a'是該索引的類型 - 'NS'的這種替代編碼允許你在常量時間內（而不是在'ks'的長度上線性化）寫函數'mapNS ::（forall k。fk - > gk） - > NS f ks - > NS g ks'！ – user2407038

如何編寫函數將泛型類型轉換爲與DSum一起使用的標記形狀類型？

回答

相關問題