具有文字和单射后继的类型级 nat？ （N-ary 组合）

Question

我将this n-ary complement 概括为n-ary 组合，但我在使界面美观时遇到了麻烦。也就是说，我不知道如何在类型级别使用数字文字，同时仍然能够对后继进行模式匹配。

滚动我自己的 nats

使用 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 求解器一样好——也就是说，我们可以信任它）。在该版本发布之前，最好避免使用类型级别的数字文字，无论它们看起来多么可爱。

Answer 2

编辑：重写答案。它变得有点笨重（而且有点马车）。

GHC 7.6

由于类型级别 Nats 在 GHC 7.6 中有些……不完整 (?)，因此实现您想要的最简单的方法是 GADT 和类型系列的组合。

{-# LANGUAGE GADTs, TypeFamilies #-}

module Nats where

-- Type level nats
data Zero
data Succ n

-- Value level nats
data N n f g where
    Z :: N Zero (a -> b) a
    S :: N n f g -> N (Succ n) f (a -> g)

type family Compose n f g
type instance Compose Zero (a -> b) a = b
type instance Compose (Succ n) f (a -> g) = a -> Compose n f g

compose :: N n f g -> f -> g -> Compose n f g
compose Z f x = f x
compose (S n) f g = compose n f . g

这种特定实现的优点是它不使用类型类，因此compose 的应用程序不受单态限制。例如，compBinRel = compose (S (S Z)) not 将在没有类型注释的情况下进行类型检查。

我们可以用一个小模板 Haskell 让它变得更好：

{-# LANGUAGE TemplateHaskell #-}

module Nats.TH where

import Language.Haskell.TH

nat :: Integer -> Q Exp
nat 0 = conE 'Z
nat n = appE (conE 'S) (nat (n - 1))

现在我们可以写compBinRel = compose $(nat 2) not，这对于更大的数字来说更令人愉快。有些人可能会认为这是“作弊”，但鉴于我们只是实现了一点语法糖，我认为没关系:)

GHC 7.8

以下适用于 GHC 7.8：

-- A lot more extensions.
{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs, MultiParamTypeClasses, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

module Nats where

import GHC.TypeLits

data N = Z | S N

data P n = P

type family Index n where
    Index 0 = Z
    Index n = S (Index (n - 1))

-- Compose is defined using Z/S instead of 0, 1, ... in order to avoid overlapping.
class Compose n f r where
    type Return n f r
    type Replace n f r
    compose' :: P n -> (Return n f r -> r) -> f -> Replace n f r

instance Compose Z a b where
    type Return Z a b = a
    type Replace Z a b = b
    compose' _ f x = f x

instance Compose n f r => Compose (S n) (a -> f) r where
    type Return (S n) (a -> f) r = Return n f r
    type Replace (S n) (a -> f) r = a -> Replace n f r
    compose' x f g = compose' (prev x) f . g
      where
        prev :: P (S n) -> P n
        prev P = P

compose :: Compose (Index n) f r => P n -> (Return (Index n) f r -> r) -> f -> Replace (Index n) f r
compose x = compose' (convert x)
  where
    convert :: P n -> P (Index n)
    convert P = P

-- This does not type check without a signature due to the monomorphism restriction.
compBinRel :: (a -> a -> Bool) -> (a -> a -> Bool)
compBinRel = compose (P::P 2) not

-- This is an example where we compose over higher order functions.
-- Think of it as composing (a -> (b -> c)) and ((b -> c) -> c).
-- This will not typecheck without signatures, despite the fact that it has arguments.
-- However, it will if we use the first solution.
appSnd :: b -> (a -> b -> c) -> a -> c
appSnd x f = compose (P::P 1) ($ x) f

但是，如源代码中所述，此实现有一些缺点。

我尝试（但失败了）使用封闭类型族来自动推断组合索引。 可能可以推断出像这样的高阶函数：

-- Given r and f, where f = x1 -> x2 -> ... -> xN -> r, Infer r f returns N.
type family Infer r f where
    Infer r r = Zero
    Infer r (a -> f) = Succ (Infer r f)

但是，Infer 不适用于具有多态参数的高阶函数。例如：

ghci> :kind! forall a b. Infer a (b -> a)
forall a b. Infer a (b -> a) :: *
= forall a b. Infer a (b -> a)

GHC 无法扩展 Infer a (b -> a)，因为它在匹配封闭族实例时不执行发生检查。如果 a 和 b 被实例化使得 a 与 b -> a 统一，GHC 将不会匹配 Infer 的第二种情况。