[Haskell-cafe] Composition of n-arity functions
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...@.
-- 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...@.
(.*) :: 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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Composition of n-arity functions
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 Dijkv.dijk@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...@.
-- 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...@.
(.*) :: 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)
