作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我试图理解使用 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 = id
但是,如果我使用元组类型的单一类型变量,则无法编译相同的定义:
ex1 :: forall (p :: (Type,Type)). Pair p -> (Fst p, Snd p)
ex1 = id
-- Ex.hs:20:7: error:
-- • Couldn't match type ‘Pair p’ with ‘(Fst p, Snd p)’
-- Expected type: Pair p -> (Fst p, Snd p)
-- Actual type: (Fst p, Snd p) -> (Fst p, Snd p)
-- • In the expression: id
-- In an equation for ‘ex1’: ex1 = id
-- • Relevant bindings include
-- ex1 :: Pair p -> (Fst p, Snd p) (bound at Ex.hs:20:1)
问题是p
可能是⊥
吗?
最佳答案
原因很简单,没有类型级别的 eta 转换检查。首先,没有机制可以将数据定义与可能具有 eta 定律的单构造函数记录/产品区分开来。我认为 p
可能是 ⊥
不是一个有效的理由。即使在部分惰性语言中,对的 eta 相等也成立(w.r.t. 观察等价)。
关于haskell - 为什么 `forall (a::j) (b::k)` 的工作方式与 `forall (p::(j,k))` 不同?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/53782842/
我是一名优秀的程序员,十分优秀!