News for hackers. Stuff that matters.
Re:Why is Idris 2 so much faster than Idris 1? by ferzul on Monday May 25, 2020 @05:20PM (#23305115)
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? by uryga on Monday May 25, 2020 @06:46PM (#23305705)
`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 <whatever that string type is>.

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? by kibwen on Monday May 25, 2020 @05:39PM (#23305257)
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.