3 ms·
Even Haskell needs an explicit language extension flag to make this happen (-XDataKinds I believe). Consider this use case data Pointer = NullPointer | No
by gamegoblin 10y ago
Even Haskell needs an explicit language extension flag to make this happen (-XDataKinds I believe).
Consider this use case
data Pointer = NullPointer | NonNullPointer Int
And I want a function that only accepts non-null pointers:
dereference :: NonNullPointer -> a
To do that and maintain my Pointer type, I'd have to do something like:
data NonNullPointer = NonNullPointer_ Int
data Pointer = NullPointer | NonNullPointer NonNullPointer
-- ^ The namespace of constructors and types is distinct,
-- so this is fine and is a constructor of Pointer that
-- contains a NonNullPointer, which only
-- has one constructor, NonNullPointer_ (note the _)
I believe -XDataKinds does something like this behind the scenes, but someone better than I should verify. I just use the above technique rather than questionable language extensions.
- dllthomas 10y agoDataKinds lets you use NullPointer and all the various NotNullPointer values as types, but they are uninhabited. It doesn't (obviously) let you restrict a parameter to values using a particular constructor of a sum type.
- gamegoblin 10y agoJust looked it up and it was GADTs I was thinking of that would allow me to do something like that.
- dllthomas 10y agoAh, yes.