Search code examples
haskellghctype-level-computation

Type level computations on types including type variables

I was working recently with freer and I got inspired to try creating a method that allows composing of arbitrary arity functions using type level computations, for example:

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

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

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

I got that working for concrete types of functions, for example, following code compiles and allows composing functions.

-- 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

However, uncommenting a Composable (a -> b) instance triggers a following compilation error:


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

I have experimented with GHCI and I think I found the root of the problem - I think that GHC doesn't reduce type level operations on types that contain type variables.

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))

I am wondering why is it so? Is there any documentation about behaviour of type variables in such context? Do you know any workarounds for this problem?

Solution

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

    That's not quite the problem. The type family TypeLevelFunctionToParams is defined by multiple clauses, and it's not clear which clause applies, since depending on whether c is a _ -> _ or not, TypeLevelFunctionToParams (a -> b -> c) might reduce using the first or second clause. Clauses in closed type families are ordered, so TypeLevelFunctionToParams (a -> b -> c) = '[a,b,c] only if c is not a function type c1 -> c2.

    Defining the "arity" of a function by "counting arrows" is fundamentally ambiguous in that way, and there is no canonical way to deal with it. In your case you might have to supply the arity upfront. You can also look for other examples of "variadic functions in Haskell" for ideas.