4 ms·

I have a few questions: a) When is the first alpha release planned ? b) Did you go the Coq/Agda route with dependent types (only total functions can be define

by Rafbill 11y ago

I have a few questions: a) When is the first alpha release planned ? b) Did you go the Coq/Agda route with dependent types (only total functions can be defined), the Haskell (once the DependentTypes extension lands) route (partial/looping functions can be used in types and may need to be evaluated at compile time, the compiler can loop, there is no associated coherent logic), or the Idris route (only total functions can be used dependently) ? c) How extensible is the Standard AST ? (e.g. would it be possible to define something like the Coq tactic interface from within the language, or through a compiler plugin ?)

wdanilo 11y ago
Hello! :) a) We will release it to the first group of alpha testers in couple of weeks from now. This will be couple of weeks, not couple of months. b) We're going the Haskell route - we allow for non-total functions, and we will extend Luna's type-checker to understand as much as possible. In fact we treat type level very similar to the value-level, very similar to the type of types - level, etc, so there could be functions evaluated at compile-time and they could cause infinite loop. Please note that although we design Luna in order to be fully dependent type language, the compiler just hit the alpha stage and there is much more work to be done in this field. c) The standard AST is really very extensible. In fact every term that belongs to AST is just different data type. We've written a library in Haskell that allows handling open sum types using all the type-level machinery to help it be bullet-proof. Luna will incorporate a library that allows you to change and manipulate the AST from within a language - something like TemplateHaskell, but without the stage restriction known from GHC. This is not available at the moment though. I doubt though you will ever need to extend the AST using a plugin, because it allows to express really wide logic, however I'm very interesting what idea do you have in your mind here! :)

by Rafbill 11y ago

wdanilo 11y ago

Hello! :) a) We will release it to the first group of alpha testers in couple of weeks from now. This will be couple of weeks, not couple of months. b) We're going the Haskell route - we allow for non-total functions, and we will extend Luna's type-checker to understand as much as possible. In fact we treat type level very similar to the value-level, very similar to the type of types - level, etc, so there could be functions evaluated at compile-time and they could cause infinite loop. Please note that although we design Luna in order to be fully dependent type language, the compiler just hit the alpha stage and there is much more work to be done in this field. c) The standard AST is really very extensible. In fact every term that belongs to AST is just different data type. We've written a library in Haskell that allows handling open sum types using all the type-level machinery to help it be bullet-proof. Luna will incorporate a library that allows you to change and manipulate the AST from within a language - something like TemplateHaskell, but without the stage restriction known from GHC. This is not available at the moment though. I doubt though you will ever need to extend the AST using a plugin, because it allows to express really wide logic, however I'm very interesting what idea do you have in your mind here! :)