問題與ISubset

Question

我有以下代碼：

type Drawable = '["object" ::: Object, "transform" ::: M44 GL.GLfloat] 
objXfrm :: "transform" ::: M44 GL.GLfloat 
objXfrm = Field 
objRec :: "object" ::: Object 
objRec = Field 

drawObject :: (Drawable `ISubset` a) => M44 GL.GLfloat -> PlainRec a -> IO() 
drawObject camera obj = 
    withVAO vao $ do 
     GL.currentProgram $= Just (program shdr) 
     setUniforms shdr (modelView =: (rGet objXfrm obj !*! camera)) 
     GL.polygonMode $= (GL.Line, GL.Line) 
     GL.drawElements GL.Triangles inds GL.UnsignedInt nullPtr 
    where Object {objVAO = vao, objNumIndices = inds, objShader = shdr} 
       = rGet objRec obj 

當我得到drawObject擺脫類型的它編譯罰款，但與I型得到

Could not deduce (IElem * ("transform" ::: V4 (V4 GL.GLfloat)) a) 
     arising from a use of `rGet' 
    from the context (ISubset * Drawable a) 
... 
    Could not deduce (IElem * ("object" ::: Object) a) 
     arising from a use of `rGet' 
    from the context (ISubset * Drawable a) 

的類型GHC推導對我來說是

drawObject 
    :: (IElem * ("object" ::: Object) rs, 
     IElem * ("transform" ::: V4 (V4 GL.GLfloat)) rs) => 
    V4 (V4 GL.GLfloat) 
    -> Rec rs Data.Functor.Identity.Identity -> IO() 

而且，作爲一個類型簽名工作正常，但一個與ISubset沒有。如果我將參數轉換爲ISubset，則錯誤完全相同。這裏發生了什麼？

Answer 1

看着乙烯基，IElem x xs（這是一個代名詞Implicit (Elem x xs)）的源代碼有兩種情況：

instance Implicit (Elem x (x ': xs)) where 
    implicitly = Here 
instance Implicit (Elem x xs) => Implicit (Elem x (y ': xs)) where 
    implicitly = There implicitly 

注意，不存在Subset這裏提及。邏輯上，(x ∈ xs) ∧ (xs ⊆ ys) ⇒ (x ∈ ys)，但由於沒有簽名Implicit (Subset xs ys), Implicit (Elem x xs) => Implicit (Elem x ys)的實例，Haskell無法推斷出適當的實例。此外，不能編寫這樣的實例，因爲這樣會導致一些令人討厭的實例重疊。

作爲一種可能的解決辦法，我們可以操縱會員證人（Elem和Subset）直接以迫使適當的情況下（這是完全未經測試，並且可能會慘遭失敗）：

{-# LANGUAGE RankNTypes, ScopedTypeVariables, and possibly more... #-} 

-- Lift an Elem value to a constraint. 
withElem :: Elem x xs -> (forall r. IElem x xs => r) -> r 
withElem Here x = x 
withElem (There e) x = withElem e x 

-- Witness of (x ∈ xs) ⇒ (xs ⊆ ys) ⇒ (x ∈ ys) 
subsetElem :: Elem x xs -> Subset xs ys -> Elem x ys 
subsetElem Here (SubsetCons e _) = e 
subsetElem (There e) (SubsetCons _ s) = There (subsetElem e s) 

-- Utility for retrieving Elem values from Fields (:::). 
fieldElem :: IElem x xs => x -> Elem x xs 
fieldElem _ = implicitly 

inSubset :: IElem x xs => x -> Subset xs ys -> (forall r. IElem x ys => r) -> r 
inSubset f s x = withElem (subsetElem (fieldElem f) s) x 

drawObject :: forall a. (Drawable `ISubset` a) => M44 GL.GLfloat-> PlainRec a -> IO() 
drawObject camera obj = 
    inSubset objRec subset $ 
    inSubset objXfrm subset $ 
     -- The desired instances should now be available here 
     ... 
    where 
    subset = implicitly :: Subset Drawable a 
    ... 

Answer 2

從簡單地看在乙烯基代碼中，似乎整個「子集」的想法還沒有完全實現（意思是說，有更多的功能和實例需要它才能真正有用）。你不能只是使用記錄之間的「子類型」關係嗎？然後，你可以做

drawObject :: (PlainRec a <: PlainRec Drawable) => M44 GL.GLfloat -> PlainRec a -> IO() 
drawObject camera obj' = 
    ... -- as before 
    where 
    obj :: PlainRec Drawable 
    obj = cast obj' 
    ... -- rest as before