[Haskell-cafe] Composition of n-arity functions

[Daniel Peebles]

As far as I can tell, it's because the NFunction type family isn't (at
least from GHC's point of view) invertible. Data families are
injective, but type families need not be, so it's quite fine for you
to write something like

type instance TypeFunction A = Q
type instance TypeFunction B = Q

Now if you try to say that TypeFunction n should unify with Q, what
should n be? There's the same issue with NFunction, in that it knows
how to make an n-ary function if you provide a type-level natural as a
parameter, but given an n-ary function, it doesn't know how to get the
type-level natural that corresponds to it back.

I don't really know of a solution to this, but it may be possible to
write an "inverse" type family to get the arity back. Not sure how
you'd tell GHC though. It'd be cool if in future we could have some
sort of annotation to declare that our type functions are injective,
without explicitly going to data families.

Hope this helps (and that I'm not completely wrong)!

Dan

On Sat, Aug 29, 2009 at 2:03 PM, Bas van Dijk<v.dijk.bas at gmail.com> wrote:
> Hello,
>
> In the levmar binding[1][2] me and my brother are working on, I need a
> function composition operator that is overloaded to work on functions
> of any arity. Basically its type needs to be something like the
> following:
>
> (.*) :: (b -> c) -> NFunction n a b -> NFunction n a c
>
> where 'NFunction n a b' represents the function 'a_0 -> a_1 -> ... -> a_n -> b'
>
> I have written the following implementation:
>
> (my question to this list is below)
>
> -- Begin -----------------------------------------------------------------------
>
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE FlexibleContexts #-}
>
> module ComposeN where
>
> --------------------------------------------------------------------------------
> -- Type-level naturals (from an idea by Ryan Ingram)
> --------------------------------------------------------------------------------
>
> data Z = Z
> newtype S n = S n
>
> type N0 = Z
> type N1 = S N0
> type N2 = S N1
> type N3 = S N2
>
> class Nat n where
>   caseNat :: forall r.
>              n
>           -> (n ~ Z => r)
>           -> (forall p. (n ~ S p, Nat p) => p -> r)
>           -> r
>
> instance Nat Z where
>   caseNat _ z _ = z
>
> instance Nat n => Nat (S n) where
>   caseNat (S n) _ s = s n
>
> induction :: forall p n. Nat n
>          => n
>          -> p Z
>          -> (forall x. Nat x => p x -> p (S x))
>          -> p n
> induction n z s = caseNat n isZ isS
>    where
>      isZ :: n ~ Z => p n
>      isZ = z
>
>      isS :: forall x. (n ~ S x, Nat x) => x -> p n
>      isS x = s (induction x z s)
>
> newtype Witness x = Witness { unWitness :: x }
>
> witnessNat :: forall n. Nat n => n
> witnessNat = theWitness
>    where
>      theWitness = unWitness $ induction (undefined `asTypeOf` theWitness)
>                                         (Witness Z)
>                                         (Witness . S . unWitness)
>
>
> --------------------------------------------------------------------------------
> -- N-arity functions
> --------------------------------------------------------------------------------
>
> -- | A @NFunction n a b@ is a function which takes @n@ arguments of
> -- type @a@ and returns a @b at .
> -- For example: NFunction (S (S (S Z))) a b ~ (a -> a -> a -> b)
> type family NFunction n a b :: *
>
> type instance NFunction Z     a b = b
> type instance NFunction (S n) a b = a -> NFunction n a b
>
> -- | @f .* g@ composes @f@ with the /n/-arity function @g at .
> (.*) :: forall n a b c. (ComposeN n) => (b -> c) -> NFunction n a b ->
> NFunction n a c
> (.*) = compose (witnessNat :: n) (undefined :: a)
>
> infixr 9 .* -- same as .
>
> class Nat n => ComposeN n where
>    compose :: forall a b c. n -> a ->
>               (b -> c) -> NFunction n a b -> NFunction n a c
>
> -- Note that the 'n' and 'a' arguments to 'compose' are needed so that the type
> -- checker has enough information to select the right 'compose' instance.
>
> instance ComposeN Z where
>    compose Z _ = ($)
>
> instance ComposeN n => ComposeN (S n) where
>    compose (S n) (_ :: a) f g = compose n (undefined :: a) f . g
>
>
> --------------------------------------------------------------------------------
> -- Test
> --------------------------------------------------------------------------------
>
> foo :: NFunction N3 Integer Integer
> foo x y z = x + y + z
>
> bar :: Integer -> Integer
> bar k = k - 1
>
> test1 = compose (witnessNat :: N3)
>                (undefined  :: Integer)
>                bar foo 1 2 3
>
> test2 = (bar .* foo) 1 2 3
>
>
> -- The End ---------------------------------------------------------------------
>
> The problem is test1 type checks and evaluates to 5 as expected but
> test2 gives the following type error:
>
> Couldn't match expected type `NFunction n a Integer'
>           against inferred type `Integer -> Integer -> Integer -> Integer'
>    In the second argument of `(.*)', namely `foo'
>
> However if I ask ghci to infer the type of (bar .* foo) I get:
>
> *ComposeN>:t (bar .* foo)
> (bar .* foo)
>  :: (Integer -> Integer -> Integer -> Integer
>        ~
>      NFunction n a Integer,
>      ComposeN n) =>
>     NFunction n a Integer
>
> Here we see that the context contains the type equality:
>
> (Integer -> Integer -> Integer -> Integer ~ NFunction n a Integer
>
> So why is ghci unable to match the expected type `NFunction n a Integer'
> against the inferred type `Integer -> Integer -> Integer -> Integer'
> while the context contains just this equality?
>
> regards,
>
> Bas
>
> [1] http://code.haskell.org/~basvandijk/code/bindings-levmar/
> [2] http://code.haskell.org/~basvandijk/code/levmar/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>