Geo*_*rge 11 haskell types higher-kinded-types parametric-polymorphism
考虑以下功能:
f :: a -> Int
f x = (1 :: Int)
我们可能会说类型f是a -> Int,f因此属于"更高级"类型.
以下哪一项是最准确的思考方式f？
其实也有一个单一 f型的a -> Int.但是,可以使用,作为f :: Int -> Int作为f :: Double -> Int,等等.
从字面上讲,类型f不是a -> Int.实际上,这只是一种简短的说法,即有一类函数f的类型是具体的(即,有一个f :: Int -> Int,一个f :: Double -> Double等等;此外,这些函数中的每一个都是彼此不同的).
同样,我们可以考虑以下类型声明:
data Maybe a = Just a | Nothing
并且问两种观点中的哪一种更正确:
没有单一的类型Maybe; 事实上,仅仅是具体类型(家族Maybe Int,Maybe String等),仅此而已.
有事实上的单一类型Maybe.这种类型是一种更高级的类型.当我们说它是一个"类型"时,我们的意思是字面意思(不是(1)的简写).碰巧我们也可以编写Maybe Int,Maybe Double等等来生成不同的类型(这恰好是具体的).但是,在这一天(即)的端部:Maybe,Maybe Int,和Maybe String表示3点不同的类型,其中两个是混凝土和其中之一是高kinded.
在Haskell中,"高级类型"真的是类型吗？或者只是具体类型"真正的类型",当我们谈论"kinded较高的类型",我们只是表示一个家庭的具体类型.此外,paramametrically多态函数是否表示单一类型的函数,或者它们仅仅表示具体类型的集合函数(仅此而已)？
小智 11
目前还不完全清楚你想要问什么,两种情况下1和2之间的实际区别是什么,但从基础数学的角度来看:
对称多态函数
f 实际上有类型 f :: forall a.a->int
对于类型化的lambda演算中的函数来说,它是完全合法的类型,它是基于Haskell的.它可以是这样的:
f = ?a:Type.?x:a.(body for f)
你怎么得到Double->Int它？您将其应用于Double键入:
f Double = (?a:Type.?x:a.(body for f)) Double => ?x:Double.(body for f|a=Double)
Haskell在场景后面执行两种操作(类型抽象和类型应用程序),尽管可以forall使用XExplicitForAllGHC扩展显式声明类型签名中的部分,并显式创建带有类型签名的Double->Int实例f:
f_double :: Double -> Int
f_double = f
更高的金属类型
考虑一个简单的类型:
data Example = IntVal Int | NoVal
(是的,是Maybe Int).
Maybe是一种类型的构造,就像IntVal是一个数据的构造.它是完全一样的东西,只是"一个水平",在意义上Maybe被应用到Type,很像IntVal被应用到Int.
在lambda演算中,Maybe有类型:
Maybe : Type->Type
Haskell不允许您从类型构造函数中获取类型,但允许您获取类型(这只是类型类型的奇特名称):
:k Maybe
Maybe :: * -> *
所以不,Maybe不是类型:你不能拥有类型的对象Maybe.Maybe(几乎)是一个从类型到类型IntVal的函数,就像从值到值的函数一样.
我们称之为应用的结果Maybe,以String作为Maybe String,就像我们所说的应用的结果IntVal,以4作为IntVal 4.
首先是一个问题:语句"所有列表都有长度"是单个语句还是一系列语句"list1有长度","list2有长度",......？
如果你给出f明确的类型forall,你得到f :: forall a. a -> Int.首先,这不是"更高级的".我们可以在GHCI中做以下事情:
?> :set -XRankNTypes
?> :k (forall a. a -> Int)
(forall a. a -> Int) :: *
所以f有一种*.
现在,在Haskell中,我们可以使用~类型相等.我们可以设置以下内容来检查GHCI中的内容:
?> :set -XImpredicativeTypes
?> :set -XTypeFamilies
?> :t undefined :: ((~) Int Int) => a
undefined :: ((~) Int Int) => a :: a
这表明GHC为这个例子找出了类型相等.类型不等式将给出以下错误:
?> undefined :: ((~) (Int -> Int) (Int)) => a
<interactive>:22:1:
Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
In the expression: undefined :: ((~) (Int -> Int) (Int)) => a
In an equation for ‘it’:
it = undefined :: ((~) (Int -> Int) (Int)) => a
现在直接使用这种方法会阻止我们比较它的类型f,但我发现了一个应该适用于我们目的的轻微变体:
?> :t undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a
undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a :: Int
换句话说,如果f是类型等价的g :: Int -> Int,那么a必须是Int.这类似于x = y,y = 0所以x = 0.我们没有x = 0指定y = 0,直到那时我们才有x = y.
Maybe 是不同的,因为它有以下类型:
?> :k Maybe
Maybe :: * -> *
因为我们正在使用DataKinds,:k (~) :: k -> k -> GHC.Prim.Constraint所以我们可以做以下事情:
?> :t undefined :: (~) Maybe Maybe => Int
undefined :: (~) Maybe Maybe => Int :: Int
?> :k Either ()
Either () :: * -> *
?> :t undefined :: (~) Maybe (Either ()) => Int
Couldn't match expected type ‘Either ()’ with actual type ‘Maybe’
总而言之,f :: forall a. a -> Int与声明一样有意义"如果你给我任何东西,我会给你一个Int".你能否把这句话翻译成一堆语句"如果你给我一只狗......","如果你给我一分钱......"？是的,但它削弱了声明.最后,准确地确定"相同"的意思,然后得到答案.