[erlang-questions] Tricky Dialyzer type

[Jesper Louis Andersen]

On Mon, Jul 20, 2015 at 9:21 AM, Raimo Niskanen <
raimo+erlang-questions@REDACTED> wrote:

> Ideas, anyone?


Your representation is icky at the type level. If possible, go for a tuple
instead since it has type A*B as a product and then this is fairly easy to
represent:

-type tagged_list(A) :: {A, [A]}.

This also opens up the possibility of sum-typing the tagged list:

-type tagged_list() ::
    {tag_a, [..]} | {tag_b, [..]}.

which in turn can hammer down the precision at which the dialyzer can work.

In naive type systems, list are homogeneous in the sense that every element
has to be drawn from the same ground type. Properly handling lists where
the "first element drives the type of the remainder of the list" is nudging
itself towards the land of dependent type theory, which the dialyzer
definitely doesn't support.

It may be possible to work with the notion of "list of two elements",
[uint8(), ty(), ...], saying that the list is a cons of uint8() followed by
one or more elements of type ty(), but I'm not sure if the dialyzer
understands this at all.



-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20150720/18e60d99/attachment.htm>