On 19/01/2012, Joachim Breitner
(I have no good idea, but here is at least one: A dot '.' as the first character indicates a type variable; compared to a ':' this is a non-capitalized character).
So that all symbols that start in dot are variables, and all others are types/constructors?
Also, is there maybe another way of distinguishing constructors and variables, besides capitalization, that works equally well for operators and non-operators? That could also help if a user would like to use unicode characters in the name of a constructor that are letters but don’t have a upper or titlecase variant. But then, this has probably been given thought a long time ago, without a better solution than capitalization resp. leading ':'.
Sometimes I thought to use "∀" to quantify over type variables, as over term variables, at least as an option.