search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Implement pragma for declaring nat optimizations #348

Open fabianhjr opened 4 years ago

fabianhjr commented 4 years ago

Helped me improve the performance of an alternative idris2 prelude I am playing with, tested with mock of ProjectEuler problem #1:

module NaiveSolution

import Prelude

import Data.Integral
import Data.Nat.Integral

main : LinkedList Nat
main = filter (`divBy` (the Nat 3)) [(the Nat 1)..100]
fabianhjr commented 4 years ago

Marceline discovered that this PR causes an explosion of memory usage while compiling Idris2 in Core/Binary (Extra ~ 5GB or so of memory usage)

edwinb commented 4 years ago

This does make the nat hack a bit less hacky, thanks! Is the compile time performance still an issue? Sometimes that can be due to ambiguity resolution going a bit out of control.

fabianhjr commented 4 years ago

Yes, there is still an issue with Idris1 compilation of Idris2.

Idris2 runs fine though.