CODEWITHSUNDEEP
value-typeidris
MWB
MWB

Reputation: 12567

Does Idris have value types?

Does Idris have value types?

The term "value type" is a bit ambiguous, but I don't know a better one.

What I mean is: Is an array/struct of structs really always an array/struct of pointers (as in Java, and unlike C# and C++)?

Upvotes: 0

Views: 398

Answers (2)

libeako
libeako

Reputation: 2384

Regarding Semantics

Value and reference types need a distinction only because of mutation. But Idris is purely functional.

Regarding Runtime Performance

"Value" types as in dotnet are usually referred to as "unboxed" in the Idris community.

AFAIK Idris does not yet support the coder's ability to declare a type unboxed. This may change in time as the language design seems to care about runtime performance.

Even if the language does not support explicit unboxing, the compiler may still do it. For example : if the runtime representation of the immutable value of a type is not bigger then that of a pointer then it is better to not box it. Note : the boxed status does not have to be decided by type. It is possible to unbox values of a type for general [immutable] usage and box some mutable usage of it.

The Idris language also has some advantage compared to dotnet regarding performance :

  • It does not have null value.
  • It has uniqueness type [in experimental stage].

The Idris back-ends are immature yet, they can be expected to miss even some basic optimization. If you are considered about runtime performance so much then now is too early to adopt Idris [though Haskell may still be a good choice]. However the language is designed with performance in mind, and i expect it to have better performance than dotnet in long time.

Upvotes: 3

eraserhd
eraserhd

Reputation: 1230

Since Idris will never mutate a value, all types are effectively value types. I'll bet this is the answer you want.

As for whether things are pointers under the hood: I know some values aren't (Int is a tagged value) and would bet that most are pointers in the C backend. This varies per backend.

Upvotes: 2

Related Questions