Hello! Basically I want to express couple of types/specs. Type parametricity is working for types:
@type functor(a) :: functor(a)
@type either(a, b) :: {:error, a} | {:ok, b}
But is not working for specs. This will not compile for some reason:
@spec fmap((a -> b), functor(a)) :: functor(b)
I don’t want to define a and b. I want them to be generic - just some type a, and some type b which might be not equal to type a.
Another question is how to do shrinking and negation on type level, for example:
@type thunk ???
@type not_a_function ???
@type curried :: (term -> curried | thunk | not_a_function)
@spec curry(function) :: curried | thunk
where thunk is a function of arity equal to zero, and not_a_function is any type except function.
Thanks for your attention.
Hi @tkachuk-labs !
I think you might want to do this:
@spec fmap((a -> b), t(a)) :: t(b) when a: term(), b: term()
About the thunk, you can do (-> integer()) for zero arity.
Recommend you these docs: Typespecs — Elixir v1.11.4
Thanks for reply and the link! I didn’t know about special syntax for zero arity function specs, it looks cool!
Also I didn’t know about guard expressions on type level, that’s awesome! Still a bit confusing, because if we will apply equational reasoning, we will get
a = term
b = term
term = term => a = b
which should not be the case for fmap
Typespecs are not Haskell-style types; trying to reason about them like they are is going to lead to confusion.
In @spec fmap((a -> b), t(a)) :: t(b) when a: term(), b: term(), term is acting as a bound - and a very loose one at that, as literally anything will satisfy it. This spec will be satisfied if fmap is given any one-arity function and any value, and promises that it will return any value.
The Erlang documentation for types can help explain this - the : operator in that when (spelled :: in Erlang) has a particular meaning and it isn’t equality:
Currently, the :: constraint (read as «is a subtype of») is the only guard constraint that can be used in the when part of a -spec attribute.
4 Likes
