是否有可能在Haskell中获得类型构造函数的种类？ [英] Is it possible to get the Kind of a Type Constructor in Haskell?

问题描述

我正在使用Data.Typeable，特别是我希望能够生成正确类型的特定类型（例如 * ）。我遇到的问题是TypeRep允许我们执行以下操作（使用GHC 7.8中的版本）：

  let maybeType = typeRep（Proxy :: Proxy Maybe）
 let maybeCon = fst（splitTyConApp maybeType）
 let badType = mkTyConApp maybeCon [maybeType] 
  

这里 badType 在某种意义上是Maybe Maybe的表示形式，它不是任何有效的类型Kind：

 > ：k也许（也许）
 
<互动>：1：8：
期待多一个参数到'Maybe'
'Maybe'的第一个参数应该是kind' *'，
，但'也许​​'有种'*  - > *'
在GHCi命令的一个类型中：也许（也许）
  

我是不想在类型层次上强制执行此操作，但我希望能够编写一个足够聪明的程序，以避免在运行时构造此类类型。我可以用 TypeRep 来完成数据级别的操作。理想情况下，我会有类似于

  data KindRep = Star | KFun KindRep KindRep 
  

并且有一个函数 kindOf 与 kindOf Int = Star （可能确实是 kindOf（Proxy :: Proxy Int）= Star ）和 kindOf Maybe = KFun Star Star ，这样我就可以类型检查我的TypeRep值。

我想我可以做到这一点手动使用类似 Typeable 的polykinded类型类型，但我宁愿不必为每件事都编写自己的实例。我还希望不要恢复到GHC 7.6，并使用不同类型的Typeable类型有单独的类型类的事实。我很乐于接受来自GHC的这些信息。

解决方案

我们可以得到一种类型，但我们需要在GHC上抛出大量语言扩展来做到这一点，包括（在这种情况下）超过可疑 UndecidableInstances 和 AllowAmbiguousTypes

  { - ＃LANGUAGE KindSignatures＃ - } 
 { - ＃LANGUAGE FlexibleInstances＃ - } 
 { - ＃LANGUAGE PolyKinds＃ - } 
 { - ＃LANGUAGE ScopedTypeVariables＃ - } 
 { - ＃LANGUAGE UndecidableInstances＃ - } 
 { - ＃LANGUAGE AllowAmbiguousTypes＃ - } 
 
 import Data.Proxy 
  

将您的定义用于 KindRep
$ p $ data KindRep = Star | KFun KindRep KindRep


我们定义 Kindable 类型可以确定的事物

  class Kindable x where 
 kindOf :: px  - > KindRep 
  

第一个例子很简单，任何类型的 * code $ Kindable ：

  instance Kindable（a： ：*）其中
 kindOf _ =星
  

获得更高类型的类型是硬。我们会试着说，如果我们能够找到它的论点的种类和将它用于论证的结果的种类，我们可以找出它的种类。不幸的是，由于它没有争论，我们不知道它的论点是什么类型;这就是为什么我们需要 AllowAmbiguousTypes 。

  instance（Kindable a，Kindable （fa））=> Kindful f where 
 kindOf _ = KFun（kindOf（Proxy :: Proxy a））（kindOf（Proxy :: Proxy（fa）））
  

结合起来，这些定义允许我们写一些类似于



  kindOf（Proxy： ：Proxy Int）= Star 
 kindOf（Proxy :: Proxy Maybe）= KFun Star Star 
 kindOf（Proxy :: Proxy（，））= KFun Star（KFun Star Star）
 kindOf（ Proxy :: Proxy StateT）= KFun Star（KFun（KFun Star Star）（KFun Star Star））
  

不要试图确定一种polykinded类型，如代理

  kindOf（Proxy :: Proxy Proxy）
  

幸运的是，有限的时间。


I am working with Data.Typeable and in particular I want to be able to generate correct types of a particular kind (say *). The problem that I'm running into is that TypeRep allows us to do the following (working with the version in GHC 7.8):

let maybeType = typeRep (Proxy :: Proxy Maybe)
let maybeCon = fst (splitTyConApp maybeType)
let badType = mkTyConApp maybeCon [maybeType]

Here badType is in a sense the representation of the type Maybe Maybe, which is not a valid type of any Kind:

> :k Maybe (Maybe)

<interactive>:1:8:
    Expecting one more argument to ‘Maybe’
    The first argument of ‘Maybe’ should have kind ‘*’,
      but ‘Maybe’ has kind ‘* -> *’
    In a type in a GHCi command: Maybe (Maybe)

I'm not looking for enforcing this at type level, but I would like to be able to write a program that is smart enough to avoid constructing such types at runtime. I can do this with data-level terms with TypeRep. Ideally, I would have something like

data KindRep = Star | KFun KindRep KindRep

and have a function kindOf with kindOf Int = Star (probably really kindOf (Proxy :: Proxy Int) = Star) and kindOf Maybe = KFun Star Star, so that I could "kind-check" my TypeRep value.

I think I can do this manually with a polykinded typeclass like Typeable, but I'd prefer to not have to write my own instances for everything. I'd also prefer to not revert to GHC 7.6 and use the fact that there are separate type classes for Typeable types of different kinds. I am open to methods that get this information from GHC.

解决方案

We can get the kind of a type, but we need to throw a whole host of language extensions at GHC to do so, including the (in this case) exceeding questionable UndecidableInstances and AllowAmbiguousTypes.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Proxy

Using your definition for a KindRep

data KindRep = Star | KFun KindRep KindRep

we define the class of Kindable things whose kind can be determined

class Kindable x where
    kindOf :: p x -> KindRep

The first instance for this is easy, everything of kind * is Kindable:

instance Kindable (a :: *) where
    kindOf _ = Star

Getting the kind of higher-kinded types is hard. We will try to say that if we can find the kind of its argument and the kind of the result of applying it to an argument, we can figure out its kind. Unfortunately, since it doesn't have an argument, we don't know what type its argument will be; this is why we need AllowAmbiguousTypes.

instance (Kindable a, Kindable (f a)) => Kindable f where
    kindOf _ = KFun (kindOf (Proxy :: Proxy a)) (kindOf (Proxy :: Proxy (f a)))

Combined, these definitions allow us to write things like

 kindOf (Proxy :: Proxy Int)    = Star
 kindOf (Proxy :: Proxy Maybe)  = KFun Star Star
 kindOf (Proxy :: Proxy (,))    = KFun Star (KFun Star Star)
 kindOf (Proxy :: Proxy StateT) = KFun Star (KFun (KFun Star Star) (KFun Star Star))

Just don't try to determine the kind of a polykinded type like Proxy

 kindOf (Proxy :: Proxy Proxy)

which fortunately results in a compiler error in only a finite amount of time.

这篇关于是否有可能在Haskell中获得类型构造函数的种类？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！