User loginNavigation 
Opposing Hierarchies of ComplexityHere is a thought for discussion: There are two models in programming 1. The machine/cpu model with pointers, addressing, manual memory allocation, modular arithmetic, floating point numbers etc. 2. The mathematical model with values, integers, real numbers etc. The code itself built up from machinecode is simplest when closest to (1), and that abstractions are built of ever increasing complexity. For example a GC is a fairly complex piece of code. Adding two stack allocated machineword ints is not. The mathematical model is built from typetheory. We can define mathematics constructively. (I am thinking more of Twelf than Coq here). It seems the type system is at its simplest expressing the fundamental concepts of mathematics, but modelling a real CPU is a complex application for typetheory (and mathematics). So a function with a simple type, has a complex implementation (involving garbage collection and layers of abstraction), and a simple function would have a complex type (possibly something involving linear refinement types, monads etc). You can see this in the difference between a simple functional language which requires a large runtime, and typed assembly language which requires a complex type system. TAL, whilst an interesting idea seems to low level fixed on a single CPU instruction architecture. So the idea is a language like 'C' with a complex type system like TAL, that can implement a pure functional DSL which would be enforced by the type system. You could have a pure strict functional language, but where a simple monadic program would compile directly to 'C' code. There should also be some proofs, for example the garbage collector implementation should result in the correct simple types for objects managed by the GC. The complex linear/effect types expressing the manual management of memory will only disappear from the type signatures if the GC code is correct. As discussed in another topic, the GC would require the language to have the capability of reflecting memory layout, stack context and concurrency control. I am interested in any work / papers that might present a similar language concept, or develop a suitable typesystem or implementation to this. By Keean Schupke at 20141017 19:36  LtU Forum  previous forum topic  next forum topic  other blogs  11079 reads

Browse archives
Active forum topics 
Recent comments
2 days 1 hour ago
2 days 12 hours ago
5 days 9 hours ago
6 days 5 hours ago
2 weeks 2 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
3 weeks 2 days ago