[Idris] Any equivalent of Haskell's newtype?

[Colin Adams]

I'm thinking about whether of not to wrap Ptrs in data types to get more
type safety. It seems like a no-brainer, but I'm not keen on adding the
slight performance hit I'd get if I used a data declaration with one
constructor, or a record with one Ptr field. Can either of these have the
overhead erased at runtime, like Haskell's newtype? Or is there another
construct?

[David Raymond Christiansen]

Hi Colin,

Post by Colin Adams
I'm thinking about whether of not to wrap Ptrs in data types to get more
type safety. It seems like a no-brainer, but I'm not keen on adding the
slight performance hit I'd get if I used a data declaration with one
constructor, or a record with one Ptr field. Can either of these have
the overhead erased at runtime, like Haskell's newtype? Or is there
another construct?

These will have the overhead erased at runtime, so you can go ahead and
use them.

In fact, it will work about as well as newtypes. That is, given:

data Wrapper = MkWrapper Ptr

and

wrap : Ptr -> Wrapper
wrap p = MkWrapper p

unwrap : Wrapper -> Ptr
unwrap (MkWrapper p) = p

you will get that wrap and unwrap have no runtime significance, but that
something like

wraps : List Ptr -> List Wrapper
wraps = map wrap

then it will still traverse the list, doing nothing at each step.

/David