On 13 July 2014 01:43, Jonathan S. Shapiro <[email protected]> wrote: > Matt, how many systems programmers do you interact with on a daily basis? Is > your opinion motivated by ample experience and qualified judgment, or do you > think that anybody will learn anything? > > Systems programmers certainly can learn HM-style type systems, and in some > cases they have. The problem today comes in two parts: (a) the languages > that use HM-style type systems are completely unsuitable to anything a > systems programmer would ever want to do (and therefore are not taken > seriously), and (b) setting that aside, the benefit of strong typing is not > seen by systems programmers. In most cases they view strong typing as an > impediment rather than a tool. > > BitC, just as it is, is an uphill battle.
It's a bit unfortunate that the only evidence we can bring to the table here is anecdotal, it's true. But it's what we have to work with. I think there are some deep insights to be had about peoples abilities to learn type systems. I really struggled with ATS for example, but that was a huge jump from a little acl2 which already felt somehow /wrong/. Not only does ATS have a phase distinction, but it has linear types and unboxed types, which means a proliferation of declarations of what are effectively datatypes, and mutability. I didn't get the 'multiple argument lists' which were frankly offensive to someone coming from python. Nevertheless, there was a point during the Agda tutorial where I realised that the way argument lists worked was /just unification/. There's really nothing more to programming and building proofs in Agda: its type system seemed far simpler than that of Haskell! When I looked at ATS again I realised it was much the same, modulo the phase distinction and linearity. Was this a failure of my study method, of the ATS tutorial, or something to do with my prejudices? I'm not really sure. Going through Edwin's video lectures on Idris - especially the one on the implementation (elaboration to a constructive type theory "TT") really cemented my understanding of constructive dependant type systems. I think that the simplicity of these systems should make them very easy to teach. I have enough 'reasonably fresh' programmers laying around that I should start attempting to validate this. Or maybe I'm an idealistic pseudo-intellectual clod, entirely detached from reality, who should go hide in the mountains with my dependent types. It's not impossible. In that case, the hope is I'll still somehow be constructive. -- William Leslie Notice: Likely much of this email is, by the nature of copyright, covered under copyright law. You absolutely MAY reproduce any part of it in accordance with the copyright law of the nation you are reading this in. Any attempt to DENY YOU THOSE RIGHTS would be illegal without prior contractual agreement. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
