8

我在玩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 比较。如何使用类型级别的自然属性在我的数据构造函数中表达这些类型的约束？

4

2 回答 2

5

TypeLists 的求解器目前不在 GHC 中，根据状态页面，它有可能在 10 月或其他时间出现在 GHC 7.8 中。

也许现在最好使用其他包。

于 2013-09-06T04:49:17.340 回答
3

这在type-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

如果将 ifmyFoo更改为 typeFoo 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
于 2013-09-06T05:32:26.497 回答