标签: forall

我开始理解forall关键字如何在所谓的"存在类型"中使用,如下所示:

data ShowBox = forall s. Show s => SB s

然而,这仅仅是如何forall使用的一个子集,我根本无法将其用于这样的事情:

runST :: forall a. (forall s. ST s a) -> a

或解释为什么这些是不同的:

foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))

或整个RankNTypes东西......

我倾向于选择清晰,无术语的英语而不是学术环境中常见的语言.我尝试阅读的大部分解释(我可以通过搜索引擎找到的解释)存在以下问题:

1. 他们不完整.他们解释如何使用这个关键字(如"生存型")的一个组成部分这让我感到高兴,直到我读使用它在一个完全不同的方式代码(比如runST,foo和bar以上).
2. 他们密集地充满了假设,我已经阅读了最新的离散数学分类,类别理论或抽象代数本周流行.(如果我再也没有读过"请参阅论文的任何细节",那就太早了.)
3. 它们的编写方式经常将简单的概念转变为曲折的语法和语法.

所以...

关于实际问题.任何人都可以完全解释的forall清晰,简单的英语关键字(或者,如果它存在于某个地方,点到我已经错过了这样一个明确的解释),不承担我在行话悠久的数学家？

编辑添加:

下面有高质量的答案有两个突出的答案,但不幸的是我只能选择一个最好的答案. 诺曼的回答很详细的和有用的,解释的方式,表现出一定的理论基础的东西forall,并在同一时间向我展示了一些它的实际影响. yairchu的回答覆盖了其他人没有提到的范围(范围类型变量),并用代码和GHCi会话说明了所有概念.我愿意选择两者是最好的.不幸的是,我不能和上,俯瞰着两个答案后密切,我已经决定,yairchu的稍微挤掉了诺曼,因为说明性代码和附加的说明.这是一个有点不公平,但是,因为我真的需要这两个答案,了解这一点是一点forall没给我留下了恐惧的隐隐感觉,当我看到它在类型签名.

如下所示,在Haskell中,可以在列表值中存储具有特定上下文边界的异构类型:

data ShowBox = forall s. Show s => ShowBox s

heteroList :: [ShowBox]
heteroList = [ShowBox (), ShowBox 5, ShowBox True]

如何在Scala中实现相同的功能,最好不要进行子类型化？

我正在努力理解与existsHaskell类型系统相关的关键字.据我所知,默认情况下Haskell中没有这样的关键字,但是:

• 在这些声明中有扩展添加它们data Accum a = exists s. MkAccum s (a -> s -> s) (s -> a)
• 我已经看过一篇关于它们的论文,并且(如果我没记错的话)它声明exists关键字对于类型系统是不必要的,因为它可以通过forall

但我甚至不明白是什么exists意思.

当我说,forall a . a -> Int这意味着(在我的理解中,不正确的一个,我猜)"对于每个(类型)a,都有一个类型的函数a -> Int":

myF1 :: forall a . a -> Int
myF1 _ = 123
-- okay, that function (`a -> Int`) does exist for any `a`
-- because we have just defined it

当我说exists a . a -> …

forall这段代码中s 的目的是什么？

class  Monad m  where
    (>>=)       :: forall a b. m a -> (a -> m b) -> m b
    (>>)        :: forall a b. m a -> m b -> m b
        -- Explicit for-alls so that we know what order to
        -- give type arguments when desugaring

(省略了一些代码).这来自Monads的代码.

我的背景:我不太懂,forall或者Haskell隐含地拥有它们.

此外,它可能并不重要,但GHCi允许我forall在给出>>类型时省略:

Prelude> :t (>>) :: Monad m => m a -> m b -> m b
(>>) :: Monad …

好的,我还有另一个Code Contracts问题.我有一个接口方法的合同,看起来像这样(为清楚起见省略了其他方法):

[ContractClassFor(typeof(IUnboundTagGroup))]
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup
{
    public IUnboundTagGroup[] GetAllGroups()
    {
        Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null));

        return null;
    }
}

我有代码消耗这样的接口:

    public void AddRequested(IUnboundTagGroup group)
    {
            foreach (IUnboundTagGroup subGroup in group.GetAllGroups())
            {
                AddRequested(subGroup);
            }
            //Other stuff omitted
    }

AddRequested需要一个非空输入参数(它实现具有需要契约的接口),所以我得到了"需要得到证实:组= NULL"在亚错误被传递到AddRequested.我正确使用ForAll语法吗？如果是这样,并在求解根本不理解,有另一种方式来帮助求解承认合同或者我只需要使用时GetAllGroups()被调用的假设？

我试图理解使用forall量化两个类型变量和使用forall量化元组类型的单个类型变量之间的区别.

例如,给定以下类型系列:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

type family Fst (p :: (a,b)) :: a where
  Fst '(a,_) = a
type family Snd (p :: (a,b)) :: b where
  Snd '(_,b) = b
type family Pair (p :: (Type,Type)) :: Type where
  Pair '(a,b) = (a,b)

我可以使用两个类型变量在对上定义一个标识,并让它在GHC 8.0.1上编译:

ex0 :: forall (a :: Type) (b :: Type). Pair '(a,b) -> (Fst '(a,b), Snd '(a,b))
ex0 …

这是 GHC 9 中的有效语法。这是什么意思（与GHC 8.10 此处要求的{..}不同）？(..)

ign :: forall {f :: Type -> Type} {p}. Applicative f => p -> f ()
ign _ = pure ()

在这个答案之后,我在我的程序中实现了一个通用的提升功能:

liftTupe :: (x -> c x) -> (a, b) -> (c a, c b) --This will error
liftTuple :: (forall x. x -> c x) -> (a, b) -> (c a, c b)

我明白的是,在此背景下,forall正在使x是任何类型的([],Maybe等.).

我现在正在研究>>=Monads 的定义:

class Applicative m => Monad m where
   (>>=) :: forall a b. m a -> (a -> m b) -> m b

我无法理解这forall在函数定义中的作用？liftTuple与之不同,它不受特定函数(x -> c x …

从ghc-8.0开始,我们有一个很好的扩展名TypeApplications.这允许我们而不是:

?> show (5 :: Int)
"5"

这样做是这样的:

?> :set -XTypeApplications
?> show @Int 5
"5"

这真的很酷.当我们添加更多类型变量时,它会变得更加复杂,但是有一些规则可以用来确定确切的顺序,并且它们有很好的记录:

showFooBar :: (Show a, Show b) => a -> b -> String
showFooBar a b = show a ++ " and " ++ show b

所以在上面的函数中我们首先提供a然后b:

?> showFooBar @Int @Double 3 4
"3 and 4.0"

这很好,但是如果我想改变订单怎么办？没问题,我们可以使用ExplicitForAll扩展(或其他一些暗示它)来指定它:

{-# LANGUAGE ExplicitForAll #-}

showFooBar :: forall b a . (Show a, Show b) => a -> b -> …

我正在使用C#4.0和Code Contracts,我有自己的自定义GameRoomCollection : IEnumerable<GameRoom>.

我想确保,任何实例GameRoomCollection都不会包含null值元素.不过,我似乎无法做到这一点.我试图做一个简单明了的例子,而不是制定一般规则.这AllGameRooms是一个实例GameRoomCollection.

private void SetupListeners(GameRoom newGameRoom) {
  Contract.Requires(newGameRoom != null);
  //...
}
private void SetupListeners(Model model) {
    Contract.Requires(model != null);
    Contract.Requires(model.AllGameRooms != null);
    Contract.Assume(Contract.ForAll(model.AllGameRooms, g => g != null));
    foreach (GameRoom gameRoom in model.AllGameRooms)
        SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 
}

任何人都可以看到,为什么我没有证明,那gameRoom不是null吗？

编辑:

在迭代之前添加对象的引用也不起作用:

IEnumerable<IGameRoom> gameRooms = model.AllGameRooms;
Contract.Assume(Contract.ForAll(gameRooms, g => g != null));
foreach (IGameRoom gameRoom in gameRooms)
    SetupListeners(gameRoom);//<= …