Parametric generics, shrinking and negation in typespecs

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.