带约束的循环类型

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)

我真的需要一个关于Typeable的foo约束

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的模式绑定。如果可以的话，我可以使用递归的let来表示如下：

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同时计算i和HiddenType 2。隐藏类型的值包括(至少部分)第一个元组元素的计算。这意味着我不希望在foo中调用两次bar (一次是为了获取HiddenType，另一次是使用该类型绑定第一个元组元素)。在存在对bar的约束的情况下，是否有办法使foo的定义成为可能？

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看作类似的东西，除了数据结构而不是函数。例如，没有ImpredicativeTypes，您可以编写：

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

它是包含t类型的所有值的列表的类型，对于一些具有Typeable约束的t。即使它是多态的，列表中的每个元素都将是相同的类型！如果您希望将forall移动到列表中，以便每个元素都可以是不同类型的t，则ImpredicativeTypes将允许这样做：

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

它不是一个通常启用的扩展，但它偶尔也很有用。

foo的非谓词版本的核心也有点不同：

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

您可以看到，如果将注释添加到x中，这将允许let按照所需的多态性。

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模式匹配下逃避。