如何使用GHC.TypeLits中的比较

我遇到了使用GHC.TypeLits的问题。 考虑下面的GADT：

data Foo :: Nat -> * where
  SmallFoo :: (n <= 2)  => Foo n
  BigFoo   :: (3 <= n)  => Foo n

我的理解是，现在对于每一个n ，类型Foo n都由一个值填充（这是一个SmallFoo或一个BigFoo，取决于n的值）。

但是如果我现在想要构造一个具体的实例如下：

myFoo :: Foo 4
myFoo = BigFoo

然后GHC（7.6.2）吐出以下错误消息：

No instance for (3 <= 4) arising from a use of `BigFoo'
Possible fix: add an instance declaration for (3 <= 4)
In the expression: BigFoo
In an equation for `myFoo': myFoo = BigFoo

这看起来很奇怪 - 我期望有一个用于这种类型级别nat比较的预定义实例。 如何使用类型级别自然表达式在我的数据构造函数中使用这些约束？

---

类型列表的求解器现在不在GHC中，根据状态页面，有一些机会会在10月份在GHC 7.8中发布。

也许现在更好地使用其他软件包。

---

这汇编在nats分支的当前头上，它应该（希望）被合并为7.8。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

module X where

import GHC.TypeLits

data Foo :: Nat -> * where
  SmallFoo :: (n <= 2)  => Foo n
  BigFoo   :: (3 <= n)  => Foo n

myFoo :: Foo 4
myFoo = BigFoo

如果myFoo被更改为Foo 1类型，它将无法编译，这可能是因为x <= y类约束被扩展为(x <=? y) ~ 'True相等约束：

$ /Source/ghc/inplace/bin/ghc-stage1 /tmp/blah.hs
[1 of 1] Compiling X                ( /tmp/blah.hs, /tmp/blah.o )

/tmp/blah.hs:16:13:
    Couldn't match type ‛3 <=? 1’ with ‛'True’
    In the expression: BigFoo
    In an equation for ‛myFoo’: myFoo = BigFoo

链接地址: http://www.djcxy.com/p/33339.html

上一篇: How to use the comparison in GHC.TypeLits

下一篇: Illegal polymorphic or qualified type using RankNTypes and TypeFamilies