[Idris] Architectural implications of type centered programming language..

[Murthy Nukala]

Hello there,

I have a few basic questions about programming with dependent types in
IDRIS. I would love to be pointed towards s answers if they are already
written up.

a. I am trying to understand why it is hard for a programming language to
support dependent types (which seem insanely useful)?

b. What are the implications of a language being 'type-centric' with
regards to the core architecture and constructs of the language as well as
the execution environment?

c. Does IDRIS expose the underlying proof structure as it compiles the
program? Is it possible to extract this (graph, tree, etc) and treat it as
a first class citizen or object?

Thanks very much. I greatly appreciate it!

Murthy

[john NeuMotiveLLC]

a. ... why it is hard for a programming language to support dependent
types ...

https://jeremywsherman.com/blog/2015/08/26/read-why-dependent-types-matter/
http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
http://software.imdea.org/~aleks/papers/ynot/ynot08.pdf

b. ... implications of a language being 'type-centric' with regards to the
core architecture ...

Garbage collection v. ref pointer & data structure management
Advantages and Disadvantages of Conservative Garbage Collection
http://www.hboehm.info/gc/issues.html

Uniqueness Types are an experimental feature available from Idris 0.9.15. A
value with a unique type is guaranteed to have *at most one* reference to
it at run-time, which means that it can safely be updated in-place,
reducing the need for memory allocation and garbage collection. The
motivation is that we would like to be able to write reactive systems,
programs which run in limited memory environments, device drivers, and any
other system with hard real-time requirements, ideally while giving up as
little high level conveniences as possible.
...
Problems/Disadvantages/Still to do...

This is a work in progress, there is lots to do. The most obvious problem
is the loss of abstraction. On the one hand, we have more precise control
over memory usage with UniqueType and BorrowedType, but they are not in
general compatible with functions polymorphic over Type.

http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html

[john NeuMotiveLLC]

https://en.wikipedia.org/wiki/Cheney%27s_algorithm