是否有可能在Haskell中获得类型构造函数?

Bri*_*ick 12 haskell type-kinds

我正在使用Data.Typeable,特别是我希望能够生成特定类型的正确类型(比方说*).我遇到的问题是TypeRep允许我们执行以下操作(使用GHC 7.8中的版本):

let maybeType = typeRep (Proxy :: Proxy Maybe)
let maybeCon = fst (splitTyConApp maybeType)
let badType = mkTyConApp maybeCon [maybeType]
Run Code Online (Sandbox Code Playgroud)

badType在某种意义上是Maybe Maybe类型的表示,它不是任何种类的有效类型:

> :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)
Run Code Online (Sandbox Code Playgroud)

我不打算在类型级别强制执行此操作,但我希望能够编写一个足够智能的程序,以避免在运行时构造此类型.我可以用数据级术语来做到这一点TypeRep.理想情况下,我会有类似的东西

data KindRep = Star | KFun KindRep KindRep
Run Code Online (Sandbox Code Playgroud)

并有一个函数kindOfkindOf Int = Star(可能是真的kindOf (Proxy :: Proxy Int) = Star),并kindOf Maybe = KFun Star Star,这样我就可以"种核对"我TypeRep值.

我想我可以使用像polykinded类型类手动这样做Typeable,但我宁愿不必编写我自己的实例.我也不想回归到GHC 7.6并使用不同类型的Typeable类型的单独类型类的事实.我对从GHC获取此信息的方法持开放态度.

Cir*_*dec 12

我们可以得到一种类型,但是我们需要在GHC中抛出一大堆语言扩展来实现这一点,包括(在这种情况下)超出可疑UndecidableInstancesAllowAmbiguousTypes.

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

import Data.Proxy
Run Code Online (Sandbox Code Playgroud)

使用你的定义 KindRep

data KindRep = Star | KFun KindRep KindRep
Run Code Online (Sandbox Code Playgroud)

我们定义了Kindable可以确定其种类的事物

class Kindable x where
    kindOf :: p x -> KindRep
Run Code Online (Sandbox Code Playgroud)

第一个例子很容易,一切*都是Kindable:

instance Kindable (a :: *) where
    kindOf _ = Star
Run Code Online (Sandbox Code Playgroud)

获得那种更高级的类型很难.我们将试图说,如果我们能够找到它的论点以及将它应用于论证的结果的类型,我们就可以找出它的类型.不幸的是,由于它没有参数,我们不知道它的参数是什么类型; 这就是我们需要的原因AllowAmbiguousTypes.

instance (Kindable a, Kindable (f a)) => Kindable f where
    kindOf _ = KFun (kindOf (Proxy :: Proxy a)) (kindOf (Proxy :: Proxy (f a)))
Run Code Online (Sandbox Code Playgroud)

结合起来,这些定义允许我们编写类似的东西

 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))
Run Code Online (Sandbox Code Playgroud)

只是不要试图确定类似的多金属类型 Proxy

 kindOf (Proxy :: Proxy Proxy)
Run Code Online (Sandbox Code Playgroud)

幸运的是,在有限的时间内导致编译器错误.