haskell - 带有文字和单射后继的类型级 nat？ (N元组成)

Question

我正在概括this n-ary complement到一个 n-ary 撰写，但我在使界面变得漂亮方面遇到了困难。也就是说，我无法弄清楚如何在类型级别使用数字文字，同时仍然能够对后继者进行模式匹配。

滚动我自己的国家

使用 roll-my-own nats，我可以使 n-ary compose 工作，但我只能将 n 作为迭代后继传递，而不是作为文字:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module RollMyOwnNats where

import Data.List (genericIndex)

-- import Data.Proxy
data Proxy (n::Nat) = Proxy

----------------------------------------------------------------
-- Stuff that works.

data Nat = Z | S Nat

class Compose (n::Nat) b b' t t' where
  compose :: Proxy n -> (b -> b') -> t -> t'

instance Compose Z b b' b b' where
  compose _ f x = f x

instance Compose n b b' t t' => Compose (S n) b b' (a -> t) (a -> t') where
  compose _ g f x = compose (Proxy::Proxy n) g (f x)

-- Complement a binary relation.
compBinRel :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel = compose (Proxy::Proxy (S (S Z))) not

----------------------------------------------------------------
-- Stuff that does not work.

instance Num Nat where
  fromInteger n = iterate S Z `genericIndex` n
-- I now have 'Nat' literals:
myTwo :: Nat
myTwo = 2
-- But GHC thinks my type-level nat literal is a 'GHC.TypeLits.Nat',
-- even when I say otherwise:
compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel' = compose (Proxy::Proxy (2::Nat)) not
{-
    Kind mis-match
    An enclosing kind signature specified kind `Nat',
    but `2' has kind `GHC.TypeLits.Nat'
    In an expression type signature: Proxy (2 :: Nat)
    In the first argument of `compose', namely
      `(Proxy :: Proxy (2 :: Nat))'
    In the expression: compose (Proxy :: Proxy (2 :: Nat)) not
-}

使用GHC.TypeLits.Nat

使用GHC.TypeLits.Nat，我得到类型级nat文字，但没有我可以找到的后继构造函数，并使用类型函数(1 +) 不起作用，因为 GHC (7.6.3) 无法推理类型函数的单射性:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module UseGHCTypeLitsNats where

import GHC.TypeLits

-- import Data.Proxy
data Proxy (t::Nat) = Proxy

----------------------------------------------------------------
-- Stuff that works.

class Compose (n::Nat) b b' t t' where
  compose :: Proxy n -> (b -> b') -> t -> t'

instance Compose 0 b b' b b' where
  compose _ f x = f x

instance (Compose n b b' t t' , sn ~ (1 + n)) => Compose sn b b' (a -> t) (a -> t') where
  compose _ g f x = compose (Proxy::Proxy n) g (f x)

----------------------------------------------------------------
-- Stuff that does not work.

-- Complement a binary relation.
compBinRel , compBinRel' :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel = compose (Proxy::Proxy 2) not
{-
    Couldn't match type `1 + (1 + n)' with `2'
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    In the expression: compose (Proxy :: Proxy 2) not
    In an equation for `compBinRel':
        compBinRel = compose (Proxy :: Proxy 2) not
-}
{-
    No instance for (Compose n Bool Bool Bool Bool)
      arising from a use of `compose'
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Note: there is a potential instance available:
      instance Compose 0 b b' b b'
-}
compBinRel' = compose (Proxy::Proxy (1+(1+0))) not
{-
    Couldn't match type `1 + (1 + 0)' with `1 + (1 + n)'
    NB: `+' is a type function, and may not be injective
    The type variable `n' is ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: Proxy (1 + (1 + 0))
      Actual type: Proxy (1 + (1 + n))
    In the first argument of `compose', namely
      `(Proxy :: Proxy (1 + (1 + 0)))'
-}

我同意semantic editor combinators这里更优雅、更通用——具体来说，编写 (.) 总是很容易。 (.). ... (n 次)而不是 compose (Proxy::Proxy n) - 但我很沮丧，因为我无法使 n-ary 组合工作符合我的预期。另外，对于 GHC.TypeLits.Nat 的其他用途，我似乎也会遇到类似的问题，例如当尝试定义类型函数时:

type family   T (n::Nat) :: *
type instance T 0     = ...
type instance T (S n) = ...

更新:已接受答案的摘要和改编

已接受的答案中发生了很多有趣的事情，但对我来说关键是 GHC 7.6 中的 Template Haskell 技巧解决方案:这可以有效地让我将类型级文字添加到我的 GHC 中7.6.3 版本，已经有单射后继者。

使用上面的类型，我通过 TH 定义文字:

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}

module RollMyOwnLiterals where

import Language.Haskell.TH

data Nat = Z | S Nat

nat :: Integer -> Q Type
nat 0 = [t| Z |]
nat n = [t| S $(nat (n-1)) |]

我已将 Nat 声明移至新模块以避免导入循环。然后我修改我的 RollMyOwnNats 模块:

+import RollMyOwnLiterals
...
-data Nat = Z | S Nat
...
+compBinRel'' :: (a -> a -> Bool) -> (a -> a -> Bool)
+compBinRel'' = compose (Proxy::Proxy $(nat 2)) not

Answer 1

不幸的是，由于最近消息中指出的一致性问题，在当前发布的 GHC 版本(GHC 7.6.3)中原则上无法回答您的问题 http://www.haskell.org/pipermail/haskell-cafe/2013-December/111942.html

尽管类型级数字看起来像数字，但不能保证它们的行为完全像数字(而且事实并非如此)。我看到 Iavor Diatchki 和同事在 GHC 中实现了正确的类型级算术(与用作后端的 SMT 求解器一样健全 - 也就是说，我们可以信任它)。在该版本发布之前，最好避免使用类型级别的数字文字，无论它们看起来多么可爱。