Indeed, there is no reason one couldn't also write a HASKCAL translator that creates TLA+ specs from a functional programming language
I thought once about that. Let's simplify your project. Let's suppose you want
to code a LISPCAL. So what do you want to create? (a) Either a lisp interpreter. But then you won't learn anything about the lisp program you want
to interpret. (b) A state machine representingt the program. Maybe it's possible and profitable. But more difficult to design than a
lisp interpreter.
For Haskell, you need to add lazyness and then I'm afraid your translation will be not understandable.
--
FL