search

purescript / purescript-typelevel-prelude

Types and kinds for basic type-level programming
BSD 3-Clause "New" or "Revised" License
63 stars 21 forks source link

Add the undefined value. #3

Closed bodil closed 7 years ago

bodil commented 7 years ago

This thing keeps being useful when I'm doing type level programming, I figured it might be relevant enough to go in typelevel-prelude.

LiamGoodacre commented 7 years ago

I'm not necessarily opposed. However this is usually dealt with using proxies, right?

succ :: forall n. Nat n => Proxy n -> Proxy (Succ n)
succ _ = Proxy
bodil commented 7 years ago

I suppose that's cleaner, but decidedly less readable. Not sure which one to prefer.

paf31 commented 7 years ago

Given that this library already uses the Proxy style elsewhere, I would rather have users define their own undefined if they want to use that style. Or in the case of functions, even unsafeCoerce unit.

In your example, aren't both types uninhabitable anyway? So an empty case would work as well, and be technically valid to boot.

LiamGoodacre commented 7 years ago

It would also only apply to types of kind Type. For example this couldn't be used for anything to do with symbols.

bodil commented 7 years ago

That makes sense.