Write a total, terminating Haskell function given a type

Question

Given a type, determine if you can write a total, terminating Haskell function.

For a type like Int -> Int, we know that the finite-precision integer type Int covers at least the range [-2^29, 2^29-1] so there are finitely many possible mappings we can have from Int to Int so we can write a total, terminating function.

For example, given the following type: (a -> b) -> (b -> c) -> (a -> c), how can I determine if we can write a total terminating function for using that type as the function signature? Or this type (a -> c) -> ((a, b) -> c).

Would greatly appreciate guidance through this problem! This is a homework question so I am only seeking guidance.

Answer 1

Given:

(a -> b) -> (b -> c) -> (a -> c)

We know that this is not necessarily partial by the Curry–Howard correspondence—interpreting -> as logical implication, product types as AND, and sum types as OR—we find it forms a tautology. But in order to find an implementation and know that it is total, we need to actually find the proof:

   (a → b) → (b → c) → a → c
-- ~~~~~~~~~~~~~~~~~~~~~~~~~
-- currying
-- ~~~~~~~~~~~~~~~~~~~~~~~~~
   (a → b) ∧ (b → c) → a → c
--           ~~~~~~~~~~~~~~~
-- currying
--           ~~~~~~~~~~~~~~~
   (a → b) ∧ (b → c) ∧ a → c
-- ~~~~~~~~~~~~~~~~~
-- commutativity of AND
-- ~~~~~~~~~~~~~~~~~
   (b → c) ∧ (a → b) ∧ a → c
--           ~~~~~~~~~~~
-- modus ponens
--           ~
   (b → c) ∧ b → c
-- ~~~~~~~~~~~
-- modus ponens
-- ~
   c → c
-- ~~~~~
-- reflexivity of implication
-- ~
   1

(This is a hypothetical syllogism.)

We can use this proof to arrive at an implementation—skipping the currying steps here, and with modus ponens corresponding to function application:

f ab bc a = bc (ab a)

The argument is similar for (a -> c) -> ((a, b) -> c) interpreting (a, b) as a ∧ b (logical AND).