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?
