-
This is really cool! I’ve always wanted to play around with a C interpreter!
I understand that it is completely impractical - but it is a shame this doesn’t support C99. I’d love to package a interpreter along with Cello because I think it would really help people learn the library a lot faster, and it suites the dynamic nature of it.
-
If you’re looking for a fully featured C interpreter there’s always CINT:
http://root.cern.ch/drupal/content/cint
It’s about 100x the code size of picoc but it claims “CINT covers most of ANSI C (mostly before C99) and ISO C++ 2003”
-
I think dependant types are a bit like an of explict formulation of many of results static analysis tools provide via data propagation. Essentially they provide different fixes to the same problem - that sometimes you want to constrain Values to avoid error conditions, not just types. I’ve not yet been persuaded that making these constraints explicit via Dependant Types is really worth the added typing and complexity. I like that static analysis tools can be used to solve lots of these issues without me having to do anything. Personally I am more interested in the development of Kinds. If you promote all constant Values and Types to Kinds you can solve some of the problems dependant types can be used for, but you also open up a bunch of cool meta-programming things also.
The “without me having to do anything” part will never be possible since you quickly get into undecidability of constraints. On the other hand, dependent types are constantly requiring less from programmers, which is really awesome - we’ll just never be able to reach the point of having some magical complete inference.
Dependent types develop kinds to be just functions at the type level. There’s no distinction, just a hierarchy, where the type of a value is
Set0and the type of that isSet1and the type of that isSet2, and so forth, to avoid Russel’s paradox.And dependent types are really brilliant at meta-programming! See the metaprogramming in Agda repository from Conor McBride or just read the Idris tutorial for lots of examples.
DT languages eliminate the distinction of kinds by creating and infinite hierarchy of types. Unless I’m mistaken about what you’re referring to.
Interesting, I feel rather the opposite. Every time I’ve used a static analysis tool it’s felt like an ad-hoc, informally-specified implementation of half a type system. (And the times when a static analysis tool can figure something out without you having to do anything correspond exactly to the times when a type system can infer a type without you having to do anything, no?)
(Kinds meanwhile are, thus far, too abstract for me to get any use out of, and I find the notation very confusing)