Haskell中存在量化值列表 [英] List of existentially quantified values in Haskell

问题描述

  { - ＃LANGUAGE ScopedTypeVariables，Rank2Types我想知道为什么这段代码没有进行类型检查： ，RankNTypes＃ - } 
 { - ＃选项-fglasgow-exts＃ - } 
 
模块Main其中
 
 foo :: [forall a。 a] 
 foo = [1] 
  

ghc抱怨：

 无法从exists5.hs：7：7 $ b中的文字'1'产生的上下文（）
中推导出（Num a） $ b  

鉴于此：

 前奏> ：t 1 
 1 ::（Num t）=> t 
前奏> 
  

似乎（Num t）上下文无法匹配arg的（）上下文。我不明白的一点是，由于（）比（数字）更普遍，所以后者应该包含前者。这与Haskell缺乏子分型支持有关吗？

感谢您对此发表任何评论。

解决方案

你在这里没有使用存在量化。您正在使用排名N的类型。

这里 [forall a。 a] 意味着每个元素必须具有所有可能的类型（不是任何，每个）。所以 [undefined，undefined] 将是该类型的有效列表，基本上就是这样。

展开有一点：如果列表的类型为 [forall a。 a] ，这意味着所有元素的类型都是 forall a。一个。这意味着任何接受任何形式参数的函数都可以将该列表的一个元素作为参数。如果你放入一个比 forall a更具体类型的元素，这不再是真的。一个，所以你不能。

要得到一个可以包含任何类型的列表，你需要用存在性定义你自己的列表类型量化。像这样：

  data MyList = Nil |全部Cons MyList 
 foo :: MyList 
 foo = Cons 1无
  

除非您限制元素类型至少实例化 Show ，否则您无法对该类型的列表执行任何操作。

I'm wondering why this piece of code doesn't type-check:

{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}

module Main where

foo :: [forall a. a]
foo = [1]

ghc complains:

Could not deduce (Num a) from the context ()
  arising from the literal `1' at exist5.hs:7:7

Given that:

Prelude> :t 1
1 :: (Num t) => t
Prelude> 

it seems that the (Num t) context can't match the () context of arg. The point I can't understand is that since () is more general than (Num t), the latter should and inclusion of the former. Has this anything to do with lack of Haskell support for sub-typing?

Thank you for any comment on this.

解决方案

You're not using existential quantification here. You're using rank N types.

Here [forall a. a] means that every element must have every possible type (not any, every). So [undefined, undefined] would be a valid list of that type and that's basically it.

To expand on that a bit: if a list has type [forall a. a] that means that all the elements have type forall a. a. That means that any function that takes any kind of argument, can take an element of that list as argument. This is no longer true if you put in an element which has a more specific type than forall a. a, so you can't.

To get a list which can contain any type, you need to define your own list type with existential quantification. Like so:

data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil

Of course unless you restrain element types to at least instantiate Show, you can't do anything with a list of that type.

这篇关于Haskell中存在量化值列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！