For example (taken from 02-Keyword--Type.purs in Jordan’s Reference):
data RunTimeType
type TypeAliasForCompileTime = RunTimeType
I looked at
purescript/documentation repo and04-Keyword--Data.purs in Jordan’s ReferenceI apologize for my eagerness if it is explained later on - tried to search for it but “data” is a pretty generic word.
It means it exists at the type level but the type has no inhabitants so no terms can be constructed for the type.
The documentation for Void gives an example of how this can be useful: https://pursuit.purescript.org/packages/purescript-prelude/4.1.1/docs/Data.Void#t:Void
It’s used in two ways:
Regarding the first one…
data TypeName = ValueName
foreign import kind TypeLevelTypeName
-- notice that there isn't a way to "construct" the below type
foreign import data TypeLevelValueName :: TypeLevelTypeName
Regarding the second one
-- `phantomType_type` isn't used in the definition of Stream
-- thus it's a "phantom" type.
data Stream phantomType_type value = Stream value
data ReadOnly
data WriteOnly
data ReadAndWrite
readStream :: forall a. Stream ReadOnly a
writeStream :: forall a. Stream WriteOnly a
readWriteStream :: forall a. Stream ReadAndWrite a
Source: https://github.com/JordanMartinez/purescript-jordans-reference/blob/latestRelease/31-Design-Patterns/03-Phantom-Types/01-What-Are-Phantom-Types.md
Real world example with better API than above example: https://pursuit.purescript.org/packages/purescript-node-streams/4.0.1/docs/Node.Stream#t:Stream
@paulyoung Thank you! I now have even more questions but given the level I’m at, they are not worth asking right now - I wouldn’t understand the answers. So mostly adding some notes here, but please feel free to ignore them; wouldn’t want to waste anyone’s time.
Also, I use hypothes.is to annotate web pages, but Pursuit doesn’t have a universal URL pointing to the latest versions, so as soon a module is updated the URL changes, and keeping track of the annotations gets harder and harder.
(stackoverflow) What’s the absurd function in Data.Void useful for?
A treasure trove of extra info: additional use cases, papers, and other insight.
(stackoverflow) How is Data.Void.absurd different from ⊥?
I had the same question looking at absurd's type signature, and how does it work? The OP quotes the implementation, and notes that absurd
is endlessly unraveling the infinite series of
Voidnewtypewrappers, and would never return even if you could find aVoidto pass it.
What I can’t wrap my head around is the comment below the question:
Barring bottom, the
absurdfunction will never be called.
So how is the rightOnly function in the example is used? That is, Void has no data values, so how would the input Either constructed in the first place?
@JordanMartinez Thank you for the concrete use cases! FFI and phantom types are still concepts I have to understand, but now I have solid examples to keep in mind.
PureScript’s primitive functions and kinds use this exact same mechanism, right? (Not sure if method one or two…) That is, the Function type is declared as data Function but it takes arguments, given that -> is syntactic sugar for Function.
You can’t get hold of a value of type Void, which means that the only way of constructing an Either Void T is to get hold of a T and apply Right to it; an Either Void T can only ever be Right.
With respect to empty data declarations: unfortunately there’s a bit of confusion around this corner of the language and I think it could do with some tidying up. There are two options for defining data types which don’t have any constructors, with slightly different syntax:
data Something (param :: Type) (otherParam :: Type)
foreign import data Something :: Type -> Type -> Type
Both of these will introduce a new data type called Something with no constructors whose kind is Type -> Type -> Type. One difference is that with the first style, you can only define types whose kind is Type (once they have had all their arguments applied), whereas with the second, you can define types of any kind.
There are two ways of interpreting either of these: they either mean that the type is uninhabited, or it is inhabited but it’s opaque, in the sense that the runtime representation isn’t visible to PureScript code and inhabitants of the type have to come from the FFI - useful for types like HTMLElement or ReactComponent.
I think everyone agrees that the foreign import data (second) style is for opaque types, but sometimes people use the first style for opaque types too. However, some other people think the first style should exclusively mean that Something is an uninhabited data type and so it should be possible to write a function absurdSomething :: forall a. Something -> a given a declaration like that. However, it’s a bit difficult to say “this should work this way and not that way,” because the FFI lets you do pretty much anything, and so the thing kind of ends up being defined by how it’s used.
The primitive types and kinds are defined in Haskell code inside the compiler, so it’s a little bit difficult to say, but if I were going to write it in PureScript code I’d write it as
foreign import data Function :: Type -> Type -> Type
since Function definitely does have inhabitants.
Thank you for the detailed replies - most of them I will have to revisit once I know more, but this sentence drove home for me what the Data.Void#absurd documentation meant by “stating that some code branch is impossible”. (Also made me remember writing similar constructs where I put something in a conditional branch that would crash the program, but wouldn’t worry about it because it could never get there - unless I messed up somewhere else.)
Thanks for expanding on this as well!
So the types declared in Prim are kind of like “placeholders”, right? (Used the double quotes because that’s the best way I can put it at the moment; don’t know anything about compilers (yet) so feel free to ignore this question if answering it would be too involved.)