Extensible Type Systems

[sirinath]

What I have been thinking is to find a way to make Frege type system extensible. This way it would be able to support Dependent Types, Dependent Object Types, and perhaps better integrate with Java Type and Type Annotation system. Additional applications could be in theorem provers.

The extensions should be achievable through Meta Programming on the user side. https://github.com/Frege/frege/issues/59

[sirinath]

https://github.com/Frege/native-gen/issues/1

[Ingo60]

This is a nice idea.

Unfortunately, it is nothing more than an idea. It is not at all clear on what type-theoretical base to do something like this and if, why and how metaprogramming (which is not there) could help here.

I must insist that the issue pages are no place for general discussions and brainstorming. Hence I ask @sirinath kindly to not open issues unless there is a bug or feature request that is well-founded in the sense that it is obvious how to implement it. For general discussions, please use the news group https://groups.google.com/forum/#!forum/frege-programming-language

[sirinath]

Since this is targeted for the JVM support of seamlessly using java from within Frege is very important. Also type annotation are around the corner.

In addition as Frege matures people might want to run languages like Idris, Agda on top of Frege as well as a means to use the results in Java.

In doing so Frege must be kept simple and maintainable so this ideally should be implemented through an language extension mechanism which might be through macros, templating and compiler plugins

[sirinath]

Some related papers:

http://homes.cs.washington.edu/~tbergan/papers/uclathesis-typmix.pdf http://www.cs.cmu.edu/~aldrich/FOOL/FOOL11/kamina04fool.pdf http://staff.aist.go.jp/y-ichisugi/epp/edoc/epp-type-check.pdf http://en.wikipedia.org/wiki/Extensible_programming http://rocketnia.wordpress.com/2013/01/29/an-extensible-type-system-for-meaning-preserving-modularity/

[talios]

On 7 Dec 2013, at 23:31, Suminda Dharmasena wrote:

In addition as Frege matures people might want to run languages like Idris, Agda on top of Frege as well as a means to use the results in Java.

Interestingly, Idris already has a java backend available to it - like Frege, it generates .java files, but also generates a pom.xml and delegates to Apache Maven for building - which is quite novel.

The FFI interface to Java is fairly nice as well:

http://janbessai.github.io/Compilation/2013/05/07/forget-scala-a-java-backend-for-idris-update/

tho, I think Frege's native FFI is cleaner.

As yet tho, I've not yet managed to get the %include/%lib Idris directives to work. Still, colour me impressed.

[Ingo60]

Yes, it is impressive. I must confess that I don't know too much about Idris, also, I am not sure what their module concept is like (i.e. how can I access things I declared in A.idr from B.idr). There are 3 possibilities: 1. you can't 2. when compiling B.idr, the compiler needs to also compile A.idr 3. upon compilation of A.idr, some information is saved somewhere so when compiling B.idr, the compiler just deserializes that info to remember what was defined in A.idr.

In Frege, we do 3.) and the information is saved in the class file itself. That is why we need (only) the class file of A when compiling B. And that is also why we can't just generate all java first and only then javac them. OTOH, as frege user you still never need to run javac manually.

I am curious how it really works, will try it out next time.