Yes, exactly. There's no way to construct a value of an arbitrary type -- outside of non-termination[1] (which doesn't really produce any values) or abuses of unsafeXXX functions. I think I perhaps should have been more explicit in my example. It could also have been specified as
f: forall a . [a] -> a
which would make it more explicit that the function has to work for any given 'a'.
[1] ... which I think I should have actually specified. The function type given does not preclude non-termination in Haskell. (You can specify such things in Idris/Coq/Agda, but the effort of implementing f can be much higher if you have to prove totality.)
[1] ... which I think I should have actually specified. The function type given does not preclude non-termination in Haskell. (You can specify such things in Idris/Coq/Agda, but the effort of implementing f can be much higher if you have to prove totality.)