包括类型变量在内的类型的类型级计算

Question

我最近在与 freer 合作，我受到启发尝试创建一种方法，允许使用类型级计算来组合任意元数函数，例如：

(+) :: Integer -> Integer -> Integer
x + y = ...

(>) :: Integer -> Integer -> Bool
x > y = ...

(sumGtThan5) :: Integer -> Integer -> Bool
sumGtThan5 x y = (+) ..> (>5)

我知道它适用于具体类型的函数，例如，以下代码编译并允许组合函数。

-- source code

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ImpredicativeTypes #-}

module Control.Pointfree where
import Data.Kind (Type)


-- | Manipulating function types

type family TypeLevelFunctionToParams fun :: [Type] where
  TypeLevelFunctionToParams (a -> b -> c -> d) = '[a, b, c, d]
  TypeLevelFunctionToParams (a -> b -> c) = '[a, b, c]
  TypeLevelFunctionToParams (a -> b) = '[a, b]

type family TypeLevelParamsToFunction params :: * where
  TypeLevelParamsToFunction '[a, b, c, d] = (a -> b -> c -> d)
  TypeLevelParamsToFunction '[a, b, c] = (a -> b -> c)
  TypeLevelParamsToFunction '[a, b] = (a -> b)


-- | Type level lists algebra
-- | Not handling empty type level lists for now. What happens if you pass one here? I don't know. Probably bad things.

type Head :: forall a. [a] -> a
type family Head xs where
  Head (x:xs) = x

type Tail :: forall a. [a] -> [a]
type family Tail xs where
  Tail (x:xs) = xs

type Last :: forall a. [a] -> a
type family Last xs where
  Last (x : '[]) = x
  Last (x:xs) = Last xs

type Init :: forall a. [a] -> [a]
type family Init xs where
  Init (x : '[]) = '[]
  Init (x:xs) = x ': Init xs

type Cons :: forall a. a -> [a] -> [a]
type family Cons x xs where
  Cons c xs = c ': xs

type Snoc :: forall a. a -> [a] -> [a]
type family Snoc x xs where
  Snoc x '[] = '[x]
  Snoc s (x:xs) = x ': Snoc s xs

-- | Composing various arity functions

type Result f = Last (TypeLevelFunctionToParams f)
type Args f = Init (TypeLevelFunctionToParams f)
type FunctionWithNewResult res f = TypeLevelParamsToFunction (Snoc res (Args f))

class Composable (f :: *) where
  (..>) :: forall res2. f -> (Result f -> res2) -> FunctionWithNewResult res2 f

instance Composable (Integer -> Bool) where
  f ..> g = g . f

instance Composable (Integer -> Integer -> Integer) where
  f ..> g = \x y -> g (f x y)

-- instance {-# OVERLAPPABLE #-} Composable (a -> b) where
--   f ..> g = g . f

-- GHCI session

ghci> import Control.Pointfree
ghci> :set -XDataKinds
ghci> :set -XPolyKinds
ghci> :set -XRankNTypes
ghci> :set -XFlexibleContexts
ghci> :set -XScopedTypeVariables
ghci> sumGtThan5 :: Integer -> Integer -> Bool = (+) ..> (>5)
ghci> sumGtThan5 2 1
False
ghci> sumGtThan5 7 3
True

但是，取消注释 Composable (a -> b) 实例会触发以下编译错误：


src\Control\Pointfree.hs:72:13: error:
    * Couldn't match type `b'
                     with `Last (TypeLevelFunctionToParams (a -> b))'
      Expected: b -> res2
        Actual: Result (a -> b) -> res2
      `b' is a rigid type variable bound by
        the instance declaration
        at src\Control\Pointfree.hs:71:31-49
    * In the first argument of `(.)', namely `g'
      In the expression: g . f
      In an equation for `..>': f ..> g = g . f
    * Relevant bindings include
        g :: Result (a -> b) -> res2
          (bound at src\Control\Pointfree.hs:72:9)
        f :: a -> b (bound at src\Control\Pointfree.hs:72:3)
        (..>) :: (a -> b)
                 -> (Result (a -> b) -> res2) -> FunctionWithNewResult res2 (a -> b)
          (bound at src\Control\Pointfree.hs:72:5)
   |
72 |   f ..> g = g . f
   |             ^

src\Control\Pointfree.hs:72:13: error:
    * Couldn't match type: TypeLevelParamsToFunction
                             (Snoc res2 (Init (TypeLevelFunctionToParams (a -> b))))
                     with: a -> res2
      Expected: FunctionWithNewResult res2 (a -> b)
        Actual: a -> res2
    * In the expression: g . f
      In an equation for `..>': f ..> g = g . f
      In the instance declaration for `Composable (a -> b)'
    * Relevant bindings include
        g :: Result (a -> b) -> res2
          (bound at src\Control\Pointfree.hs:72:9)
        f :: a -> b (bound at src\Control\Pointfree.hs:72:3)
        (..>) :: (a -> b)
                 -> (Result (a -> b) -> res2) -> FunctionWithNewResult res2 (a -> b)
          (bound at src\Control\Pointfree.hs:72:5)
   |
72 |   f ..> g = g . f

我试验过 GHCI，我想我找到了问题的根源 - 我认为 GHC 不会减少对包含类型变量的类型的类型级操作。

GHCi, version 9.0.1: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Control.Pointfree ( src\Control\Pointfree.hs, interpreted )
Ok, one module loaded.
ghci> import Control.Pointfree
ghci> :set -XDataKinds
ghci> :set -XPolyKinds
ghci> :set -XRankNTypes
ghci> :set -XFlexibleContexts
ghci> :set -XScopedTypeVariables
ghci> :kind! Integer -> Integer
Integer -> Integer :: *
= Integer -> Integer
ghci> :kind! Integer -> Integer -> Bool
Integer -> Integer -> Bool :: *
= Integer -> Integer -> Bool
ghci> :kind! forall a b. a -> b
forall a b. a -> b :: *
= a -> b
ghci> :kind! Init (TypeLevelFunctionToParams (Integer -> Integer))
Init (TypeLevelFunctionToParams (Integer -> Integer)) :: [*]
= '[Integer]
ghci> :kind! Init (TypeLevelFunctionToParams (Integer -> Integer -> Integer))
Init (TypeLevelFunctionToParams (Integer -> Integer -> Integer)) :: [*]
= '[Integer, Integer]
ghci> :kind! forall a b c. Init (TypeLevelFunctionToParams (a -> b -> c))      
-- NOT REDUCED!
forall a b c. Init (TypeLevelFunctionToParams (a -> b -> c)) :: [*]
= Init (TypeLevelFunctionToParams (a -> b -> c))

我想知道为什么会这样？在这种情况下是否有关于类型变量行为的文档？您知道这个问题的解决方法吗？

Answer 1

GHC doesn't reduce type level operations on types that contain type variables.

这不是问题所在。类型族 TypeLevelFunctionToParams 由多个子句定义，不清楚哪个子句适用，因为根据 c 是否是 _ -> _，TypeLevelFunctionToParams (a -> b -> c) 可能会减少使用第一条或第二条。封闭类型族中的子句是有序的，因此仅当 c 不是函数类型时 TypeLevelFunctionToParams (a -> b -> c) = '[a,b,c] c1 -> c2。

通过“计数箭头”来定义函数的“元数”从根本上来说是模棱两可的，并且没有规范的方法来处理它。在您的情况下，您可能必须预先提供数量。您还可以查找“Haskell 中的可变参数函数”的其他示例以获取灵感。

包括类型变量在内的类型的类型级计算

Type level computations on types including type variables

haskell

ghc

type-level-computation