带约束条件的循环打字

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模式匹配下退出。