Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why is Idris 2 so much faster than Idris 1?

type-driven.org.uk

Post reply on HN
Print view View original

21–30 of 88 posts

Re: Why is Idris 2 so much faster than Idris 1?

#21

Post by ferzul »

kibwen wrote: post #19
heinrich-lunge wrote: post #13

Earlier quoted context omitted.

Dependent types are a language feature, simply adding two types --- the dependent product / exponential / function type, and the dependent sum / product / tuple type. You can definitely add dependent types to Rust, but I see at least the following problems. 1. Rust compile times and dependent typing compile times are both really long. Combining the two sounds like it'd be unacceptably long. 2. Rust promises full type…

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

correct me if i'm wrong - i only spent a hours with rust: doesn't dbg! run at compile time? and therefore your example is still compatible with type erasure?

Re: Why is Idris 2 so much faster than Idris 1?

#22

Post by kibwen »

TeMPOraL wrote: post #20
kibwen wrote: post #19

Earlier quoted context omitted.

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

Isn't this just compile-time dispatching? I think types 'inaccessible at runtime but still affecting generating code' are table stakes, and basically half of the point of doing these types of generics. Equivalent C++ code (admittedly, C++ templates aren't really generics) would have enough information to shove literal 4 and 16 into the binary there.

This is kind of my point, I've never heard the term "type erasure" used with static dispatch (and Rust code, for better or worse, overwhelmingly prefers static dispatch to dynamic dispatch).

Rust does guarantee type erasure on lifetimes, but lifetimes are only used for semantic analysis, and are completely separate from and unrelated to code generation/type layout.

Re: Why is Idris 2 so much faster than Idris 1?

#23

Post by kibwen »

ferzul wrote: post #21
kibwen wrote: post #19

Earlier quoted context omitted.

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

correct me if i'm wrong - i only spent a hours with rust: doesn't dbg! run at compile time? and therefore your example is still compatible with type erasure?

I'm asking what we're referring to by "type erasure" here; one can use trait objects to erase a type in Rust, and size_of (which, yes, runs at compile-time (the debug macro is just for printing, not for const eval)) does indeed work on such type-erased objects, but it will always give you the size of the fat pointer to the trait object.

Re: Why is Idris 2 so much faster than Idris 1?

#24

Post by mokus »

chongli wrote: post #15
dependenttypes wrote: post #9

Earlier quoted context omitted.

> because neither of them have Turing-complete type checkers https://sdleffler.github.io/RustTypeSystemTuringComplete/

That's almost certainly a bug. At any rate, a proper language with dependent types does not have a Turing-complete type checker and that's what makes it magical. You get incredible power without having to worry about non-termination in your type checker.

Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense.

For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number. You now have a type that is, for all practical purposes, Turing-complete, even though it is theoretically guaranteed to terminate.

Re: Why is Idris 2 so much faster than Idris 1?

#25

Post by Jweb_Guru »

dependenttypes wrote: post #9
chongli wrote: post #6

Earlier quoted context omitted.

You mean you could write a compiler for Idris (or any other dependent typed language) in a Turing complete language. That’s fine but it’s not a very useful statement. If you want dependent types IN Rust or Swift then Turing-completeness won’t help you, because neither of them have Turing-complete type checkers. You’d have to modify the compiler for them (and thus change the language itself).

> because neither of them have Turing-complete type checkers https://sdleffler.github.io/RustTypeSystemTuringComplete/

Sure, and there exists a dependent type system in Rust's trait system. It is wildly impractical to actually use, interacts poorly with the actual language, and a great example of why Turing Completeness of a type system means very little in practice.

Re: Why is Idris 2 so much faster than Idris 1?

#27

Post by [deleted] »

TeMPOraL wrote: post #20
kibwen wrote: post #19

Earlier quoted context omitted.

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

Isn't this just compile-time dispatching? I think types 'inaccessible at runtime but still affecting generating code' are table stakes, and basically half of the point of doing these types of generics. Equivalent C++ code (admittedly, C++ templates aren't really generics) would have enough information to shove literal 4 and 16 into the binary there.

[deleted]

Re: Why is Idris 2 so much faster than Idris 1?

#28

Post by uryga »

ferzul wrote: post #21
kibwen wrote: post #19

Earlier quoted context omitted.

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

correct me if i'm wrong - i only spent a hours with rust: doesn't dbg! run at compile time? and therefore your example is still compatible with type erasure?

`dbg!(x)`, being a macro, expands to something at compile time; at runtime, that expanded code will do something like `write(x.fmt(), stderr)`. it's not relevant here, only `size_of` is.

what's happening here is that rust does "monomorphization" – it generates two versions of `foo`, one for ints and one for strings; then, in each specialized version, `size_of` is specialized to that particular type's implementation of `size_of` (compiler-generated), which returns 4 for i32 and 16 for .

i'm sure it's actually more nuanced than that, but i think that's the general principle.

Re: Why is Idris 2 so much faster than Idris 1?

#29

Post by chongli »

mokus wrote: post #24
chongli wrote: post #15

Earlier quoted context omitted.

That's almost certainly a bug. At any rate, a proper language with dependent types does not have a Turing-complete type checker and that's what makes it magical. You get incredible power without having to worry about non-termination in your type checker.

Guaranteed termination of a sound dependent type system is only useful as a mathematical property, not a practical one (yes, I know the mathematical consequences have practical benefit but I mean directly it doesn’t say anything about what a typical user thinks of as “termination”). You could still trivially write an algorithm at the type level which is Turing-complete in a practical sense. For example, write a type…

For example, write a type that implements a Turing machine parameterized by a program and a natural number N of evaluation steps to take. Apply that type to Graham’s number or some suitably large natural number.

To do that you’d first need to be able to fit Graham’s number into your source code which unfortunately is never going to happen.

Idris has a termination checker which in practice rejects non-primitive recursion. If you can’t prove to the type checker that your recursive function deferments toward a base case at every step then your program won’t type check. So there’s no back-door method to get Graham’s number or other silliness like the Ackerman function into your types.

Re: Why is Idris 2 so much faster than Idris 1?

#30

Post by Reelin »

TeMPOraL wrote: post #20
kibwen wrote: post #19

Earlier quoted context omitted.

> Rust promises full type erasure when you're not using "dyn" I don't know if "type erasure" is the accurate term to use with the generic-specialization scheme that Rust uses; one can trivially write a generic Rust function that demonstrates that types, while inaccessible at runtime, still semantically affect the generated code: use std::mem::size_of; fn foo (t: T) { dbg!(size_of:: ()); } fn main() { foo(1); // print…

Isn't this just compile-time dispatching? I think types 'inaccessible at runtime but still affecting generating code' are table stakes, and basically half of the point of doing these types of generics. Equivalent C++ code (admittedly, C++ templates aren't really generics) would have enough information to shove literal 4 and 16 into the binary there.

What do you mean by C++ templates not really being generics? Aren't Rust's generics also implemented as templates (as opposed to parametric polymorphism)?
Post reply on HN