(no subject)
Sep. 15th, 2015 08:11 amIn a language enjoying relational parametricity each fresh symbol must immediately obtain either a value (therefore automatically also a type) or at least a type, otherwise it cannot be used in any sensible way. So there are two freshness markers for a symbol: a definition or a type declaration.
I don't believe in languages where whitespaces can be ignored at random. :-(
P.S. If you want variable type to be inferred, there is a notation n : ¤.
x : Type # that's a type declaration y: value # that's a definition
I don't believe in languages where whitespaces can be ignored at random. :-(
P.S. If you want variable type to be inferred, there is a notation n : ¤.