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 a root of the problem - 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?
CodePudding user response：
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.