歡迎!

這裡是 Elixir Taiwan 的部落格。我們自 2014 開始舉辦每個月定期的實體聚會,目前持續運作中,聚會詳情請參考 facebook/meetup 連結。這裡我們會分享各種程式相關的新聞、知識與新議題。

Posts

Feb 18 2025

2025/02/18 Meetup 筆記

Interesting Find #

  • PhoenixAnalytics Awesome looking analytics tool for your pet project.

  • Success Typing vs Set Theoretic Types

    Elixir 1.18 changelog around types.

    From ChatGPT

    link

    Deep Dive into Set-Theoretic Types in Elixir #

    Since we’ve seen how Elixir’s current type system (using Dialyzer) allows some incorrect types to slip through, let’s now explore how a set-theoretic type system would work differently.


    1. How Would Set-Theoretic Types Work in Elixir? #

      A **set-theoretic type system** introduces explicit operations like **union (`|`), intersection (`&`), and negation (`~`)**. These allow us to **strictly enforce** type constraints **at compile time** rather than relying on Dialyzer’s success typing.
    

    🔹 Comparison with Dialyzer #

      | Feature               | Dialyzer (Success Typing) | Set-Theoretic Types (Strict Typing) |
      |----------------------|----------------------|-------------------|
      | **Union Types (`\|`)**    | Implicit, inferred   | Explicit & enforced |
      | **Intersection Types (`&`)** | Not supported       | Fully supported |
      | **Negation Types (`~T`)**    | Not supported       | Supported (`~String`) |
      | **Compile-Time Checks**     | No (only warnings)   | Yes (strict enforcement) |
      | **Error Handling**    | Some false negatives | More precise detection |
    

    2. Example: Strict Union Types in Set-Theoretic Typing #

      Let’s redefine the previous example **using set-theoretic types**.
    

    🔸 Current Elixir (Dialyzer) #

      ```elixir
      @spec format_value(integer() | binary()) :: binary()
      def format_value(value) do
        to_string(value)
      end
      ```
    
      ❌ **Problem:** Dialyzer won’t stop you from passing an atom like `:world`, even though the spec only allows `integer()` or `binary()`.
    
      ---
    

    🔹 How It Would Work in a Set-Theoretic Type System #

      If Elixir had **explicitly enforced union types**, the function might be written like this:
    
      ```elixir
      def format_value(value: Integer | String) -> String do
        to_string(value)
      end
      ```
    
      ✅ **Key Differences:**
      - **Explicit union (`Integer | String`)** prevents invalid inputs at **compile-time**.
      - **If you pass a `List` or an `Atom`, compilation will fail.**  
      - **No need for Dialyzer!** Type checking is built-in.
    
      ---
    

    3. Intersection Types (&) #

      Sometimes we want a type that **must satisfy multiple conditions**. Right now, Elixir **doesn't support this**.
    

    🔸 Current Elixir (No Intersection Types) #

      Imagine we have `Drawable` and `Clickable` behaviors:
    
      ```elixir
      defmodule Drawable do
        @callback draw() :: :ok
      end
    
      defmodule Clickable do
        @callback click() :: :ok
      end
      ```
    
      If we want to define a function that only accepts objects that **both** implement `Drawable` and `Clickable`, there's no **native** way to enforce this.
    

    🔹 With Set-Theoretic Types (&) #

      ```elixir
      def handle_element(element: Drawable & Clickable) -> :ok do
        element.draw()
        element.click()
      end
      ```
    
      ✅ **Key Differences:**
      - `Drawable & Clickable` means **the argument must satisfy both interfaces.**
      - If an object **implements only `Drawable` but not `Clickable`, it’s rejected**.
      - **Stronger compile-time safety** without runtime checks.
    
      ---
    

    4. Negation Types (~T) #

      Another powerful feature of set-theoretic types is **negation**: `~T` means “any type **except** `T`.”
    

    🔸 Current Elixir (No Negation Types) #

      Imagine we have a function that **should accept any type except a string**:
    
      ```elixir
      def process_value(value) do
        case value do
          s when is_binary(s) -> raise "Strings not allowed!"
          _ -> IO.inspect(value)
        end
      end
      ```
    
      ❌ **Problem:** We have to write explicit guards (`is_binary/1`).  
      ❌ **If we forget the guard, there's no type-level protection.**
    

    🔹 With Set-Theoretic Types (~T) #

      ```elixir
      def process_value(value: ~String) -> any do
        IO.inspect(value)
      end
      ```
    
      ✅ **Key Differences:**
      - `~String` ensures **compile-time rejection of strings**.
      - No need for **manual guards**.
      - Stronger **error prevention** at the type level.
    
      ---
    

    5. Practical Implications: How Could Elixir Adopt This? #

      For Elixir to move towards **set-theoretic types**, it would require:
      1. **Replacing or Enhancing Dialyzer** – Since Dialyzer is based on success typing, a **new type checker** would be needed.
      2. **Compiler Support for Explicit Types** – Instead of type specs as comments (`@spec`), **types would be enforced at compile-time**.
      3. **Backwards Compatibility Strategy** – Since Elixir doesn’t require types today, introducing stricter types must be **gradual**.
    
      ---
    

    6. Would This Be Worth It? #

      ✅ **Pros:**
      - **Better Type Safety** – More precise types prevent subtle runtime errors.
      - **No More False Negatives** – Unlike Dialyzer, which sometimes **misses errors**, strict typing **catches them at compile time**.
      - **More Expressive Code** – Explicit union, intersection, and negation types make type contracts **clearer**.
    
      ❌ **Cons:**
      - **More Rigid** – Developers who like Elixir’s **dynamic nature** might dislike stricter typing.
      - **Potentially More Boilerplate** – If types **must** be declared everywhere, it could slow down development.
    
      🚀 **José Valim’s research into set-theoretic types suggests that Elixir might move in this direction!** But it would need to balance type safety with Elixir’s dynamic flexibility.
    
  • Chris McCord is working on AI code generation

Jan 5 2025

為什麼要學函數式語言

GenAI 興起的現在,為什麼還要學新語言?