帶約束條件的循環打字

Question

在下面的示例中，我試圖使foo返回其「預期」多態輸出類型。想法是foo返回一個多態值和一個存在類型，然後bar指定元組的類型爲隱藏類型。 （當然，這只是工作，如果在bar種類也存在，這是真的在我的情況）以下示例編譯：

{-# LANGUAGE GADTs, ScopedTypeVariables #-} 

module Foo where 

import Data.Proxy 
import Data.Typeable 

data HiddenType where 
    Hidden :: (Typeable a) => Proxy a -> HiddenType 

foo :: (i,HiddenType) 
foo = (undefined, Hidden (Proxy::Proxy Int)) 

data Foo where 
    Foo :: i -> Foo 

bar :: Foo 
bar = 
    let (x,h) = foo 
    in case h of 
    (Hidden (p::Proxy i)) -> Foo (x :: i) 

我真的需要foo一個Typeable約束：

foo :: (Typeable i) => (i,HiddenType) 

當我再補充一點約束（沒有其他變化），我得到這些錯誤：

Foo.hs:20:15: 
    No instance for (Typeable t0) arising from a use of ‘foo’ 
    The type variable ‘t0’ is ambiguous 
    Relevant bindings include x :: t0 (bound at Foo.hs:20:8) 
    Note: there are several potential instances: 
     instance [overlap ok] Typeable() 
     -- Defined in ‘Data.Typeable.Internal’ 
     instance [overlap ok] Typeable Bool 
     -- Defined in ‘Data.Typeable.Internal’ 
     instance [overlap ok] Typeable Char 
     -- Defined in ‘Data.Typeable.Internal’ 
     ...plus 14 others 
    In the expression: foo 
    In a pattern binding: (x, h) = foo 
    In the expression: 
     let (x, h) = foo 
     in case h of { (Hidden (p :: Proxy i)) -> Foo (x :: i) } 

Foo.hs:22:35: 
    Couldn't match expected type ‘a’ with actual type ‘t0’ 
     because type variable ‘a’ would escape its scope 
    This (rigid, skolem) type variable is bound by 
     a pattern with constructor 
     Hidden :: forall a. Typeable a => Proxy a -> HiddenType, 
     in a case alternative 
     at Foo.hs:22:6-24 
    Relevant bindings include 
     p :: Proxy a (bound at Foo.hs:22:14) 
     x :: t0 (bound at Foo.hs:20:8) 
    In the first argument of ‘Foo’, namely ‘(x :: i)’ 
    In the expression: Foo (x :: i) 
Failed, modules loaded: none. 

我明白，約束變成共同的論點所以在我看來，這裏的問題是GHC無法處理GADT的模式綁定。如果可以，我可以用一個遞歸讓利給這樣說：

bar :: Foo 
bar = 
    let (x :: i,h) = foo 
     (Hidden (p::Proxy i)) = h 
    in Foo x 

這應該使範圍的限制，提供額外的參數foo。我在這裏的目的是使h包含一些（隱藏）具體類型i，它應作爲具體類型的多態函數 GHC抱怨：

Foo.hs:19:8: 
    You cannot bind scoped type variable ‘i’ 
     in a pattern binding signature 
    In the pattern: x :: i 
    In the pattern: (x :: i, h) 
    In a pattern binding: 
     (x :: i, h) = foo 

Foo.hs:20:8: 
    My brain just exploded 
    I can't handle pattern bindings for existential or GADT data constructors. 
    Instead, use a case-expression, or do-notation, to unpack the constructor. 
    In the pattern: Hidden (p :: Proxy i) 
    In a pattern binding: (Hidden (p :: Proxy i)) = h 
    In the expression: 
     let 
     (x :: i, h) = foo 
     (Hidden (p :: Proxy i)) = h 
     in Foo x 

我使用情況下的假設是 1. foo 2.同時計算i和HiddenType 2.隱藏類型的值涉及（至少部分）第一個元組元素的計算。這意味着我做而不是想在bar中撥打foo兩次（一次獲得HiddenType，並且一次使用該類型綁定第一個元組元素）。 在foo上存在約束時，是否有某種方法可以使bar的定義成爲可能？

Answer 1

我想問題是foo的返回值實際上並不是多態。 foo本身是多態的，但返回值必須存在於特定類型中。不幸的是，您要使用的類型尚不可用，並且由於有循環參考，因此無法在foo的呼叫站點處列入範圍。如果我們寫出來的僞核心的foo定義，這個問題是清楚的：

foo (@ iType) _ = (undefined @ iType, HiddenType...) 

這裏@ iType是一種說法。在獲取HiddenType之前，我們需要首先完成foo的類型應用程序（和字典應用程序，這是未使用的），因此無法按原樣執行此操作。

幸運的是，有辦法說服GHC是foo應該返回一個實際的多態值：

{-# LANGUAGE GADTs, ScopedTypeVariables #-} 
{-# LANGUAGE ImpredicativeTypes #-} 

module Foo where 

import Data.Proxy 
import Data.Typeable 

data HiddenType where 
    Hidden :: (Typeable a) => Proxy a -> HiddenType 

foo :: (forall i. Typeable i => i,HiddenType) 
foo = (undefined, Hidden (Proxy::Proxy Int)) 

data Foo where 
    Foo :: i -> Foo 

bar = 
    let (x,h) = foo 
    in case h of 
    Hidden p -> Foo (x `asProxyTypeOf` p) 

如果你熟悉較高等級的類型（例如RankNTypes擴展名），你能想到的ImpredicativeTypes作爲類似的東西，except for data structures instead of functions。例如，如果沒有ImpredicativeTypes你可以寫：

list1 :: forall t. Typeable t => [t] 

它是一個包含t類型的所有值，對於一些t與Typeable約束列表的類型。即使它是多態的，列表中的每個元素都將是相同的類型！相反，如果你要移動的forall名單內，讓每一個元件可以是不同類型的t，ImpredicativeTypes將允許這樣的：

list2 :: [forall t. Typeable t => t] 

這不是一個支持常用擴展，但它是偶爾有用。

爲foo的impredicative版本的核心是有點不同，以及：

foo = (\(@ iType) _ -> undefined @ iType, HiddenType...) 

你可以看到，這允許您添加註釋到letx是爲所需多：

bar :: Foo 
bar = 
    let (x :: forall i. Typeable i => i,h) = foo 
    in case h of 
    Hidden p -> Foo (x `asProxyTypeOf` p) 

這允許您在隱藏類型中延遲x的實例化，直到它可用時爲止。儘管如此，您仍然需要在Foo或另一個Hidden範圍內進行裝箱，因爲ghc不允許類型在第一個Hidden模式匹配下退出。