Hi Jeremy, >My dominant recollection is the difficulty of getting the system to do the >right type inference, and getting terms to typecheck. I was forever working >out where I needed to put in type annotations.
In Coq and Mizar I don't have this experience, in the sense that I hardly ever need type annotations where I don't expect them. In occasionally have problems with "match ... with ..." typing, getting that to work can be very frustrating. But apart from that, I don't have much of a problem. >It led me to conclude that the systems offering automatic inference of a >principal type really occupy a "sweet spot", ie the best compromise between >ease of use and expressive power. I don't mind so much explicitly typing my variables where they are bound. So I don't share this feeling of Hindley-Milner style polymorphism being a "sweet spot". I'd rather have full polymorphism and dependent types as well. Freek ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
