On 4 July 2014 03:12, Jonathan S. Shapiro <[email protected]> wrote: > On Wed, Jul 2, 2014 at 12:19 PM, Geoffrey Irving <[email protected]> wrote: >> In terms of your worry about shapes, the issue with dependent typing >> is that there is no "now compile time is done" point in a fully >> dependent typed language where you know what n is in Vec n a. That >> is, there is no hard striation between compile time and runtime. > > > Yes. And that is why a fully dependent type system is not the right path for > a systems programming language.
There are many dependent type systems where there is no visible distinction, but the distinction is clearly syntactic in ATS, and somewhat obvious in Idris (which will warn you if you use something that it thinks should be erased: https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis ). The lack of phase distinction is certainly *not* a direct consquence of having fully dependent types and similar static and dynamic expression languages. I personally think ATS' approach is better from a systems perspective, but there may be other ways of getting the same result. -- 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
