Again, can't speak for haskell. In agda you usually have 2 goals creating a function * Proving a property of some other object. In this case you have to write

Again, can't speak for haskell. In agda you usually have 2 goals creating a function * Proving a property of some other object. In this case you have to write the type first since type is the theorem you want to prove, and implementation is the proof. * Implement a transformation. In this case, as you described you might get away first writing the impl, and then the type, but I personally never even attempt to do that since writing out the type gives me a lot to think about the implementation of the transformation. Once types are explicit, implementation usually ends up being a lot more obvious.