Domanda
I'm pretty new to Haskell and I have created a high-order function:
forAll f ls ls2 = all (`f` ls) ls2
I need to specify the type, but I have doubts with the type of the function f:
GHCi says it's:
forAll :: (a -> t -> Bool) -> t -> [a] -> Bool
But shouldn't it be something like this?
forAll :: (a -> t) -> t -> [a] -> Bool
Thanks.
Soluzione
No, since all has the type
https://stackoverflow.com/questions/22950399
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russianall :: (a -> Bool) -> [a] -> Bool
f has to return Bool. Since
(`f` ls)
(\a -> a `f` ls)
flip f ls
f must take an element of the list, ls, and produce a Bool. Making it's type
f :: a -> t -> Bool
Where ls :: t and ls2 :: [a].
Altri suggerimenti
Let's examine the type you suspect this function must take.
The type (a -> t) means that given some a we can produce a t. We have some as in our list of as, [a] and so we can presumably make a bunch of ts with a type like [t]. Further, we have yet another t passed in which we can stick in that other bunch of [t]s as well.
Now, I call these as and ts because we really don't know anything about what their actual types are. That said, we do know what our goal is: we must produce a Bool.
So somewhere inside our function must be a method of converting a bunch of ts, like [t], into a Bool. We could do this with something like length ts > 3 but I doubt that's what you're looking for.
The function type that GHC provides you looks a bit different. It states that we have a way of taking an a and a t together to a Bool (the type is (a -> t -> Bool)). Since we have a list of as we can feed each one of them one after another into this function so long as we have a source of ts. Since we have exactly one t coming in, we'll need to use it each time. Altogether that gives us a bunch of Bools, a [Bool] even. This is exactly the kind of thing we're looking for, though, as we'd like to condense that list of [Bool] to a single Bool using all.
This kind of narrative of types I've laid out—where we talk about functions having and wanting values, like a game of give and take between you and your program—is a pretty common method of reasoning about the types of your programs. You can often get quite far with this kind of exploration and provide yourself a lot of justification for the types of programs you've constructed.
Ultimately, GHC is always going to be "right" about the type of the particular values you ask it about—that's the advantage of an Hindley Milner type system. Try to check the types of functions that GHC infers often and see whether GHC has deduced some detail of the type narrative that you've missed.
(By the way, that narrative I mention is called, perhaps obviously, "game semantics of programs" and it also shows up in proofs and logic. There's a much deeper tie there if you decide to follow it.)
