Почему диализатор не обнаруживает этот плохой тип?


Диализатор ведет себя довольно странно для меня в этом случае, и я не нашел ничего, чтобы лучше понять его.

Это не ошибка:

defmodule Blog.UserResolver do
  @type one_user :: ( {:error, String.t} )

  @spec find(%{id: String.t}, any()) :: one_user

  def find(%{id: id}, _info) do
    age = :rand.uniform(99)
    if (age < 100) do
      # This doesn't trigger a type error, even though it's wrong
      {:ok, %{email: "dw@1g.io", name: "Deedub"}}      
    else 
    {:error, "Age isn't in the right range"}
    end
  end
end
Обратите внимание, что одна из возможных ветвей возврата определенно не совпадает с сигнатурой типа.

Это, однако, имеет ошибку:

defmodule Blog.UserResolver do
  @type one_user :: ( {:error, String.t} )

  @spec find(%{id: String.t}, any()) :: one_user

  # Throws an error since no return path matches the type spec
  def find(%{id: id}, _info) do
    age = :rand.uniform(99)
    if (age < 100) do
      {:ok, %{email: "dw@1g.io", name: "Deedub"}}      
    else 
     10
    end
  end
end

В этом случае ни одна из возможных ветвей не соответствует typespec, и dialyzer говорит, что имеет это сообщение об ошибке:

web/blog/user_resolver.ex:4: Invalid type specification for function 'Elixir.Blog.UserResolver':find/2. The success typing is (#{'id':=_, _=>_},_) -> 10 | {'ok',#{'email':=<<_:64>>, 'name':=<<_:48>>}}

Часть I не понимаю, что диализатор ясно распознает два разных типа, которые могут возвращать ветви ((#{'id':=_, _=>_},_) -> 10 | {'ok',#{'email':=<<_:64>>, 'name':=<<_:48>>}), поэтому это не проблема вывода. Так почему же тогда он не признает, что одна из ветвей не соответствует спецификации типа (кажется, он будет счастлив, если только одна ветвей соответствует, что совсем не то, что я хочу)

1 2

1 ответ:

Из ссылки LearnYou , которую предоставил Догберт, dialyzer будет:

Жалуются только на ошибки типа, которые гарантируют сбой.

В первом примере, если возраст всегда больше или равен 100, функция возвращает объявленный тип. Во втором примере функция не может вернуть объявленный тип.

dialyzer создает набор уравнений ограничений. Если есть какое-либо решение этих уравнений, то диализатор не будет жаловаться. Erlang был создан как динамически типизированный язык. dialyzer - это просто программа, которую кто-то написал постфактум. По причинам, которые, я уверен, они обдумывали, обсуждали и теоретизировали, дизайнеры dialyzer выбрали эту функциональность.

Я ищу более строгую проверку типов, если это возможно.

Пока невозможно:

Система Типа Эрланга

Причина отсутствия более сложной системы типов заключается в том, что нет от эрлангские изобретатели знали, как его написать, поэтому он так и не был создан. То преимущество системы статического типа заключается в том, что ошибки могут быть предсказаны при время компиляции, а не во время выполнения, что позволяет сбоям быть выявляется раньше и фиксируется по более низкой цене. У многих людей есть пытался построить систему статического типа для Эрланга. К сожалению, из-за проектные решения, принятые, когда был изобретен Эрланг, ни один проект не был реализован. способен написать комплексную систему типов, так как с помощью горячего кода погрузка, это по сути своей сложно. Процитируем Джо Армстронга в одна из многих систем типа flame wars, " похоже, так и должно быть "легко" - и действительно, за несколько недель программирования можно сделать типовую систему, которая обрабатывает 95% языка. Несколько человеко-лет работы [некоторыми из самые яркие умы в области компьютерных наук] пошли в попытке исправить остальные 5% - но это действительно сложно."

Из "Erlang Programming (Francesco Cesarini & Simon Thompson)".

A test suite требуется, чтобы держать динамически типизированные программы под контролем. Эликсир - это всего лишь Рубиновая версия Эрланга. Ruby также является динамически типизированным языком, но у него нет диализатора. Единственное, что есть у Руби-это тестирование. Вы используете наборы тестов, чтобы держать Дикий Запад языков программирования под контролем-не компилятор. Если вам нужен статически типизированный язык, то Рубифицированная версия Erlang не была отличным выбором-см. Haskell.