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)
并有一个函数kindOf与kindOf Int = Star(可能是真的kindOf (Proxy :: Proxy Int) = Star),并kindOf Maybe = KFun Star Star,这样我就可以"种核对"我TypeRep值.
我想我可以使用像polykinded类型类手动这样做Typeable,但我宁愿不必编写我自己的实例.我也不想回归到GHC 7.6并使用不同类型的Typeable类型的单独类型类的事实.我对从GHC获取此信息的方法持开放态度.
Cir*_*dec 12
我们可以得到一种类型,但是我们需要在GHC中抛出一大堆语言扩展来实现这一点,包括(在这种情况下)超出可疑UndecidableInstances和AllowAmbiguousTypes.
{-# 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)
幸运的是,在有限的时间内导致编译器错误.
| 归档时间: |
|
| 查看次数: |
349 次 |
| 最近记录: |