0

I was wondering if there is any better way for finding FUNCTIONS given only TYPE of it in Haskell. Ex.-

Find function for given type- (a->b->c) ?

Always I have to think hard in a brute force manner. please help.

I have gone through this - Haskell: Deducing function from type, but could not find a better way.

Improve this question
6
  • No, I only have type and pen-paper or ghc installed. Now deduce the function Commented Nov 22, 2013 at 1:33
  • 1
    Are you familiar with djinn? It performs this exact task... and is written in Haskell. Commented Nov 22, 2013 at 1:37
  • 4
    You can use the same method as djinn does; prove a theorem in intuitionistic propositional logic. Commented Nov 22, 2013 at 1:39
  • Actually it can be a type of custom made function. In that case, it won't give me the answer. And I was preparing for some exam thats why I was asking Commented Nov 22, 2013 at 1:39
  • The method used by djinn can absolutely be applied to "a type of a custom made function". That said I'll be quite now that 1) this is clearly off topic for SO 2) the author of Djinn has appeared. Commented Nov 22, 2013 at 1:41

3 Answers 3

Reset to default
2

It's sometimes possible. For instance, we all know that there are no "proper" values with type forall a. a and only one with type forall a . a -> a, but there are an infinite number of ones with type forall a. (a -> a) -> a -> a.

In particular, you can think of some Haskell types as expressing theorems in type theory and the process of instantiating them as the process of proving that theorem. There's no general method for doing this, but there are a number of tautological types like forall a . a -> a which have easily discoverable proofs.

To learn much more about this process, consider reading Software Foundations by Benjamin Pierce or Certified Programming with Dependent Types by Adam Chlipala. These two both explore how to prove theorems (instantiate types) like this using the language Coq which is similar to Haskell being based on OCaml.

Improve this answer
Sign up to request clarification or add additional context in comments.

2 Comments

It's worth noting that your original function, a -> b -> c is impossible to construct without "cheating" (using undefined or similar). Trivial proof: If it existed suppose it was called foo. Then (foo :: () -> () -> a) () () :: a which means we can create any type. This also means we can prove types that are logically falsy like Void.
To reinforce this from the logical point of view, the function with type (a -> b) cannot exist without cheating already. The type reads, as a logical statement, that "If A then B" for all "A" and "B". "If it is snowing outside, then 2+2=5", "If the sky is blue, then I can fly", and so on. Compare that with the trivial type forall a . a -> a which is "proven" by id :: forall a . a -> a. As logic that says "If A, then A" for all "A"... which actually makes sense. "If pigs can fly, then pigs can fly", "If I can go faster than the speed of light, then I can go faster than the speed of light"
1

Besides DJINN (which is an external tool), you can also use the following code

http://okmij.org/ftp/Haskell/types.html#de-typechecker

to, informally, convert a type into a value, within Haskell. You can immediately invoke this function.

Improve this answer

Comments

0

I guess .. (\x y -> (x,y) ) can fit into the type (a->b->c)

Improve this answer

2 Comments

I believe you misunderstand the question. The question is more of "give me a function that can be given this type signature". I can use a function typed a -> b -> c in a case demanding Int -> Float -> Double, but I can't use your function in that case.
I get it.. So the function with the signature a->b->c can be (\x y -> undefined)

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.