On Dec 7, 2007 6:27 AM, Victor Nazarov wrote:

Cool solution and not so complicated and ad-hoc. But I'd like to ask isn't the following definition is more natural and simple?

nary 0 x [] = x nary n f (x:xs) | n > 0 = nary (n-1) (f $ read x) xs

Sometimes it helps to write type signatures for functions. As in this case, where you'll find you won't be able to... :-) Luke

This is great! Two questions: 1) I want to make sure the function arity matches the list length (as a runtime check). I think I can do this with an arity function using Data.Typeable. I came up with: arity f = a (typeOf f) where a tr | typeRepTyCon tr /= mkTyCon "->" = 0 | otherwise = 1 + (a . fromJust . funResultTy tr . head . typeRepArgs $ tr) This looks awful. Is there a better way to get the function arity? 2) Once I have say arity (+) == 2 at runtime, how can I get it reified into Succ (Succ Zero)) at compile time to be able to use it as the first argument in your nary function? Can/should I use Template Haskell for this? Dan Victor Nazarov wrote:

...

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}

data Zero data Succ a

class Nary n x y | n x -> y where nary :: n -> x -> [String] -> y

instance Nary Zero x x where nary _ x [] = x

instance (Nary n y z, Read x) => Nary (Succ n) (x->y) z where nary _ f (x:xs) = nary (undefined::n) (f $ read x) xs

Luke Palmer wrote:

You can project the compile time numbers into runtime ones:

Yes, that works well if I know a priori what the arity of the function is. But I want to be able to have the compiler deduce the arity of the function (e.g. by applying undefined until it is no longer a function), precisely so I don't have to supply it myself. Function arity is (I think) something already known to GHC, so I don't know why we can't get at it too.

On Dec 7, 2007 6:21 PM, Dan Weston wrote:

...

This is great! Two questions:

1) I want to make sure the function arity matches the list length (as a runtime check). I think I can do this with an arity function using Data.Typeable. I came up with:

arity f = a (typeOf f) where a tr | typeRepTyCon tr /= mkTyCon "->" = 0 | otherwise = 1 + (a . fromJust . funResultTy tr . head . typeRepArgs $ tr)

This looks awful. Is there a better way to get the function arity?

2) Once I have say arity (+) == 2 at runtime, how can I get it reified into Succ (Succ Zero)) at compile time to be able to use it as the first argument in your nary function? Can/should I use Template Haskell for this?

You can project the compile time numbers into runtime ones:

...

class ProjectN n where projectN :: n -> Int

instance ProjectN Zero where projectN _ = 0

instance (ProjectN n) => ProjectN (Succ n) where projectN _ = 1 + projectN (undefined :: n)

And then make sure the length matches the projected number of arguments. Other disagreements will be resolved at compile time.

Luke

...

Dan

Victor Nazarov wrote:

...

...

{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} data Zero data Succ a

class Nary n x y | n x -> y where nary :: n -> x -> [String] -> y

instance Nary Zero x x where nary _ x [] = x

instance (Nary n y z, Read x) => Nary (Succ n) (x->y) z where nary _ f (x:xs) = nary (undefined::n) (f $ read x) xs

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Dec 7, 2007 7:57 PM, Luke Palmer wrote:

On Dec 7, 2007 7:41 PM, Dan Weston wrote:

...

Luke Palmer wrote:

...

You can project the compile time numbers into runtime ones:

Yes, that works well if I know a priori what the arity of the function is. But I want to be able to have the compiler deduce the arity of the function (e.g. by applying undefined until it is no longer a function), precisely so I don't have to supply it myself.

Function arity is (I think) something already known to GHC, so I don't know why we can't get at it too.

No, it is not. Consider:

compose f g x = f (g x)

What is the arity of f?

Oh, you're saying at run-time, given an object. Still no, by some definition. compose f g = f . g compose' f g x = f (g x) Are you saying that these two exactly equivalent functions should have different arity? If not, then is the arity 2 or 3? Luke

On Dec 7, 2007 8:39 PM, Dan Weston wrote:

...

compose f g = f . g

compose' f g x = f (g x)

Are you saying that these two exactly equivalent functions should have different arity? If not, then is the arity 2 or 3?

Prelude> :t let compose f g = f . g in compose let compose f g = f . g in compose :: (b -> c) -> (a -> b) -> a -> c Prelude> :t let compose' f g x = f (g x) in compose' let compose' f g x = f (g x) in compose' :: (t -> t1) -> (t2 -> t) -> t2 -> t1

The arity is the number of top-level ->

Both are arity 3.

Hmm, this still seems ill-defined to me. compose :: (Int -> Int -> Int) -> (Int -> Int) -> Int -> Int -> Int Is a valid expression given that definition (with a,b = Int and c = Int -> Int), but now the arity is 4. Luke

Questioning apfelmus definitely gives me pause, but...

id :: a -> a -- "arity" 1 id = ($) :: (a -> b) -> (a -> b) -- "arity" 2

I agree with the arities given above (but without quotes) and see no ill-definedness to arity. But these are two different classes of functions. There are arguments of the first function that cannot be applied to the second (e.g. 5). The fact that the two have different type signatures shows that Haskell can distinguish them (e.g. in the instantiation of a type class). The difficulties of Haskell's type system in the presence/intersection of ad hoc/parametric polymorphism is an orthogonal issue. I think that every function application must have a unique monomorphic type at the call site of the "arity" function (assisted or not by type annotation), and this type is known to converge in a Template Haskell construction.

We have to specialize the type of id before supplying it to wrap . For example,

wrap (id :: Int -> Int)

works just fine.

The necessity of type annotation/restriction is an orthogonal issue to the above. Am I missing something more fundamental? apfelmus wrote:

Luke Palmer wrote:

...

Hmm, this still seems ill-defined to me.

compose :: (Int -> Int -> Int) -> (Int -> Int) -> Int -> Int -> Int

Is a valid expression given that definition (with a,b = Int and c = Int -> Int), but now the arity is 4.

That's correct, the arity of a function is not well-defined due to polymorphism. The simplest example is probably

id :: a -> a -- "arity" 1 id = ($) :: (a -> b) -> (a -> b) -- "arity" 2

Therefore, the polymorphic expression

wrap id

is problematic. It roughly has the type

wrap id ~~ [String] -> a

But it's clearly ambiguous: do we have

wrap id (x:_) = read x

or

wrap id (f:x:_) = wrap ($) (f:x:_) = read f (read x)

or what? (assuming a read instance for function types) GHCi gives it a type

...

:type wrap id wrap id :: (FunWrap (a -> a) y) => [String] -> y

but trying to use it like in

...

let x = wrap id ["1"] :: Int

yields lots of type errors. We have to specialize the type of id before supplying it to wrap . For example,

wrap (id :: Int -> Int)

works just fine.

I don't like this behavior of wrap since it violates the nice property of polymorphic expressions that it's unimportant when a type variable is instantiated, like in

map ((+1) :: Int -> Int) [1..5] = map (+1) ([1..5] :: [Int]) = (map (+1) [1..5]) :: [Int]

Regards, apfelmus

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Dan Weston wrote:

Questioning apfelmus definitely gives me pause, but...

Don't hesitate! :) Personally, I question everyone and everything, including myself. This is a marvelous protection against unintentionally believing things just because I've heard them several times like "Monads are hard" or "Haskell code is easier to understand", but has many more uses. As Feynman put it: "What do you care what other people think?"

...

id :: a -> a -- "arity" 1 id = ($) :: (a -> b) -> (a -> b) -- "arity" 2

I agree with the arities given above (but without quotes) and see no ill-definedness to arity.

But these are two different classes of functions. There are arguments of the first function that cannot be applied to the second (e.g. 5).

The fact that the two have different type signatures shows that Haskell can distinguish them (e.g. in the instantiation of a type class).

No, I think not. Having different type signatures is not enough for being distinguishable by type classes. The second type ∀a,b. (a -> b) -> a -> b is an instance of the first one ∀a. a -> a "Instance" not in the sense of class instance but in the sense of type instance, i.e. that we can obtain the former by substituting type variables in the latter, here a := (a -> b). Formally, we can write this as an "inequality" ∀a. (a -> a) < (a -> b) -> a -> b with "x < y" meaning "x less specific than y" or "x more general than y". Now, the property I meant with

...

I don't like this behavior of wrap since it violates the nice property of polymorphic expressions that it's unimportant when a type variable is instantiated is that the class instance predicate is monotonic with respect to the type instance relation: from x < y and Num x , we can always conclude Num y . In particular, let's examine a type class

class Nat a => Arity a f | f -> a describing that the function type f has a certain arity a which is expressed with Peano numbers in the type system: data Zero = Zero data Succ a = Succ a type One = Succ Zero type Two = Succ One class Nat n instance Nat Zero instance Nat n => Nat (Succ n) Now, if Arity One (∀a . a -> a) is true then due to monotonicity, Arity One ((a -> b) -> a -> b) must be true, too! The only possible solution to this dilemma is to drop the class instance for (∀a. a -> a). It's no problem to have many special instances Arity One (Int -> Int) Arity One (Char -> Char) etc. but we can't have the polymorphic one. In other words, not every (potentially polymorphic) function type has a well-defined arity! Oleg's hack basically supplies all those possible particular instances while avoiding the polymorphic one. Concerning the ill-definedness of wrap id

...

...

:type wrap id wrap id :: (FunWrap (a -> a) y) => [String] -> y

but trying to use it like in

...

let x = wrap id ["1"] :: Int

yields lots of type errors. We have to specialize the type of id before supplying it to wrap . For example,

wrap (id :: Int -> Int)

works just fine.

which I don't like, it seems that I have to life with it. That's because the toy implementation class FunWrap f x | f -> x where wrap :: f -> [String] -> x instance FunWrap (Int -> Int) Int where wrap f [x] = f (read x) instance FunWrap ((Int -> Int) -> Int -> Int) Int where wrap f [g,x] = f id (read x) already shows the same behavior. When trying something like

wrap id ["1"] :: Int

, GHCi complains that there's no polymorphic instance FunWrap (a -> a) Int There can't be, since that would disallow the special instances and moreover conflict with the functional dependency. So, wrap id is an example of an essentially ill-typed expression that the type checker does not reject early (namely when asking for its type). Regards, apfelmus

jerzy karczmarczuk wrote:

apfelmus:

...

As Feynman put it: "What do you care what other people think?"

It was not Feynman, but his wife.

Thanks, I should have questioned my claim :) Regards, apfelmus