The foundation of this effort, the programming language Idris by Edwin Brady. Idris is basically the answer to the question: "What would Haskell look like if it had full dependent types?" It has strict semantics but also offers annotations for non-strict evaluation. If you want to know more about Idris can highly recommend the tutorial. Sadly there is not a lot of material out there to learn about programming with dependent types but I will link some resources in this blog post.
How to use it:
module Main product : List Integer -> Integer product = foldl (*) 1 fac : Integer -> Integer fac n = product [1..n] main : IO () main = print (fac 300)
and compile it
and run it
> node test.js … long output is long …
As you can see, the backend also supports big integers. The generated file is completely self contained including code from the standard library like typeclasses etc. (not everything but the code you need).
module Main product : List Integer -> Integer product = foldl (*) 1 fac : Integer -> Integer fac n = product [1..n] alert : String -> IO () alert s = mkForeign (FFun "alert" [FString] FUnit) s main : IO () main = alert $ show (fac 300)
Compile and run it in a browser of your choice ^^
- Certified Programming With Dependent Types
- Talk by Andreas Bogk at Chaos Communication Camp 2011
- Agda Wiki