Hi Mario,
Slightly off-topic, I had experience with the type system of HOL-Omega
(system F, if I recall the terminology right, not dependent types, so my
experience may not be very relevant)
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. Quite
frustrating after my experience with regular HOL, and Isabelle.
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.
Cheers,
Jeremy Dawson
On 06/10/17 03:46, Mario Castelán Castro wrote:
On 04/10/17 20:09, Ramana Kumar wrote:
Perhaps it would make more sense to ask people who are using rich type
systems what their motivations are :)
(On this list it's probably mostly people who are satisfied with simple
type theory.)
Yes, you are right. I wrote to this list because I am interesting in the
opinion of informed “outsiders”, not only “insiders”, so to speak.
------------------------------------------------------------------------------
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
------------------------------------------------------------------------------
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
