[erlang-questions] Tricky Dialyzer type

[Raimo Niskanen]

On Mon, Jul 20, 2015 at 10:06:32AM +0200, Jesper Louis Andersen wrote:
> 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:

Unfortunately that is not possible since the tagged tuple already has
another meaning in the code I am trying to add this feature to.  This was
the "exhausted option" I briefly mentioned.  I should have stated that
explicitly in my question...

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

That's a pity.  For me it is just about two different kinds of wrappers.
Obviously I am not a type expert.

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

At least list(type(), type()) and [type(), type()] both gives syntax errors
so it seams that Dialyzer does not understand that at all.

> 
> 
> 
> -- 
> J.

> _______________________________________________
> erlang-questions mailing list
> erlang-questions@REDACTED
> http://erlang.org/mailman/listinfo/erlang-questions


-- 

/ Raimo Niskanen, Erlang/OTP, Ericsson AB