In your second point about type level functions, I don't understand what you mean when you say
Therefore, to ensure that type checking
itself terminates, functions which are not total are treated as
constants at the type level, and do not evaluate further.
Particularly does a function treated as a constant mean that it cannot represent multiple types e.g. Bool (True/False), if we were to only define the case for True.
Coming from OOP seeing the word constant in there threw me off.
|