标签: polykinds

f1和之间有什么区别f2？

$ ghci -XRankNTypes -XPolyKinds
Prelude> let f1 = undefined :: (forall a        m. m a -> Int) -> Int
Prelude> let f2 = undefined :: (forall (a :: k) m. m a -> Int) -> Int
Prelude> :t f1
f1 :: (forall            (a :: k) (m :: k -> *). m a -> Int) -> Int
Prelude> :t f2
f2 :: (forall (k :: BOX) (a :: k) (m :: k -> *). m a -> …

我编写了一个Const3非常类似的newtype Const,但包含三个给定类型参数中的第一个:

newtype Const3 a b c = Const3 { getConst3 :: a }

我可以为这个新类型定义很多有用的实例,但我必须自己完成所有这些.

但是,我在类型级别上应用的功能类似于该功能

\a b c -> a

这@pl告诉我相当于const . const.

双方(.)并const具有匹配的NEWTYPE包装:Compose和Const.所以我想我能够写:

type Const3 = Compose Const Const

并自动继承有用的实例,例如:

instance Functor (Const m)
instance (Functor f, Functor g) => Functor (Compose f g)
-- a free Functor instance for Const3!

但GHC不同意:

const3.hs:5:23:
    Expecting one more argument to ‘Const’
    The first argument of …

当我在做haskell-excercises问题时。我看到以下代码Constraint通过将每种类型应用于 Constraint 构造函数来创建聚合。在 GHC 中，Constraints 的深层嵌套元组似乎仍然是一种Constraint（也许是扁平化的？）。

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


type family All (c :: Type -> Constraint) (xs :: [Type]) :: Constraint where
  All c '[] = ()
  All c (x ': xs) = (c x, All c xs)

-- >>> :kind! All
-- All :: (* -> Constraint) -> [*] -> Constraint
-- = All

-- >>> :kind! …

多金属型应用是否是内射的？

当我们能PolyKinds,我们知道f a ~ g b意味着f ~ g和a ~ b？

动机

当试图回答另一个问题时,我将问题减少到只有PolyKinds启用时才收到以下错误.

Could not deduce (c1 ~ c)
from the context ((a, c z) ~ (c1 a1, c1 b))

如果多金属型应用是单射的,我们可以推导c1 ~ c如下.

(a,   c z) ~ (c1 a1,   c1 b)
(a,) (c z) ~ (c1 a1,) (c1 b) {- switch to prefix notation -}
      c z  ~           c1 b  {- f a ~ g b …

用户2426021684的评论让我调查是否有可能提出一个类型函数,以证明对于某些和:FF c1 c2 fafa

1. fa ~ f a
2. c1 f
3. c2 a

事实证明,最简单的形式很容易.但是,我发现很难弄清楚如何编写多角度版本.幸运的是,当我写这个问题时,我设法找到了一种方法.

浏览各种软件包的haddocks我经常会看到这样的实例文​​档(Control.Category):

Category k (Coercion k)
Category * (->)

或者这个(Control.Monad.Trans.Identity):

MonadTrans (IdentityT *)

这种签名究竟意味着什么呢？它没有出现在源代码中,但我已经注意到它似乎发生在使用PolyKinds扩展的模块中.我怀疑它可能像TypeApplication但有一种类型.因此,例如最后一个示例意味着IdentityT如果它的第一个参数具有类型,则它是monad变换器*.

所以我的问题是:

• 我的解释是否正确以及签名所涉及的具体内容是什么？
• 在第一个Category例子中,我怎么知道这k是一种而不是一种类型？或者我只是要知道这个Category？
• 这段语法的源代码是什么？

我不是要求各种解释.

我遇到了由 Happy 生成的看似无效的代码。问题归结为 GHC 没有推断函数的多类类型签名。下面是一个例子：

{-# Language MagicHash #-}\n\nf x = ()\n\nmain = pure (f 1#)\n

由于 GHC 正在推断f :: a -> ()哪里a :: *，所以失败了

 \xe2\x80\xa2 Couldn't match a lifted type with an unlifted type\n   When matching the kind of \xe2\x80\x98GHC.Prim.Int#\xe2\x80\x99\n \xe2\x80\xa2 In the first argument of \xe2\x80\x98f\xe2\x80\x99, namely \xe2\x80\x981#\xe2\x80\x99\n   In the first argument of \xe2\x80\x98pure\xe2\x80\x99, namely \xe2\x80\x98(f 1#)\xe2\x80\x99\n   In the expression: pure (f 1#)\n

是否有任何语言编译指示我可以打开来编译此代码？我知道理论上我可以只添加类型签名，但是，由于这是由 Happy 生成的代码，我不希望手动修改任何内容。

我有两个类型系列,其中一个类型映射一种类型到另一种类型的不同类型和多态函数:

{-# LANGUAGE PolyKinds, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-} 

type family F (a :: k1) :: k2
type family G (a :: k2) :: *

f :: forall k1 k2 (a :: k1) (p :: k1 -> *) . p (a :: k1) -> G (F (a :: k1) :: k2)
f = undefined

此代码没有检查以下错误消息:

• Couldn't match type ‘G k20 (F k20 k1 a)’ with ‘G k2 (F k2 k1 a)’
  Expected type: p a -> G k2 (F k2 …

我有以下表示类别的类别，其中对象类别由一种种类表示，每个hom类由一种由上述种类的类型索引的类型表示。

{-# LANGUAGE GADTs, DataKinds, KindSignatures, PolyKinds #-}

type Hom o = o -> o -> *

class GCategory (p :: Hom o)
  where
  gid :: p a a
  gcompose :: p b c -> p a b -> p a c

一个实例的简单示例是：

instance GCategory (->)
  where
  gid = id
  gcompose = (.)

现在，我要对产品类别进行建模。作为一个简单的起点，下面是一个类型，它对->与本身的乘积相对应的类别的词素进行建模：

data Bifunction ab cd
  where
  Bifunction :: (a -> c) -> (b -> d) -> Bifunction '(a, b) '(c, d)

这是相应的操作：

bifunction_id :: Bifunction …

我收到一个错误

app\Main.hs:1:1: error:
    Couldn't match kind `*' with `Constraint'
    When matching types
      b :: *
      (Set b, Set s) :: Constraint
  |
1 | {-# LANGUAGE TypeFamilies #-}
  | ^

不知道为什么b和约束(Set b, Set s)是匹配的？我希望约束能够对类型 b 进行存在量化，但为什么它会匹配它们呢？

I believe the last thing I changed before getting the error was adding OpOutcome to the class.

here is the code

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DataKinds …

假设我有一种类型l :: * -> * -> *，所以我需要应用 2 种类型a，并b获得一个简单的类型l a b。

如何将类型映射l :: * -> * -> *到新类型m(l) :: * -> * -> *，其中的m(l) b a含义与l a bfor each相同a,b？这里a,b不是常数。是否可以？这么想有错吗？