# 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.

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