关于Idris与Haskell中胖箭头（=>）语法选择差异的技术问询

Great question! I’ve wondered about this syntax split too, since Idris borrows so heavily from Haskell but makes this deliberate choice to separate -> and => across different contexts. The short answer is: yes, this syntax decision absolutely comes from recognizing practical value in clearly distinguishing between type-level declarations and implementation-level definitions.

Let’s break down the reasoning:

1. Visual and Cognitive Clarity #

The most immediate benefit is readability. In Idris:

• -> is exclusively used in type signatures to denote function types (e.g., foo : Int -> String means "foo takes an Int and returns a String").
• => is used in implementation code:
  • Lambda expressions: \x => show x (reads as "given x, return show x")
  • Case branches: case n of 0 => "Zero" (reads as "if n matches 0, return 'Zero'")

This split lets you instantly parse whether you’re looking at a type description or concrete logic, even in long, nested code. In Haskell, where both contexts use ->, you have to rely on surrounding syntax (like \ for lambdas or :: for type signatures) to tell them apart—small but cumulative cognitive load, especially when working with dependent types where type and implementation code can interleave more closely.

2. Semantic Distinction #

Beyond readability, the symbols reinforce a subtle but important semantic difference:

• -> in type theory represents the function space—the set of all possible functions from type A to type B. It’s a declarative statement about what a function is.
• => represents a binding or pattern match resolution—it’s an imperative-like statement about what a function does when given specific inputs or patterns.

Idris, as a language designed to lean into dependent typing and precise semantics, uses syntax to make these conceptual differences explicit. It’s a small choice that aligns with Idris’s overall philosophy of making code’s intent as clear as possible.

3. Avoiding Ambiguity (and Future-Proofing) #

While Haskell doesn’t have major ambiguity issues with overusing ->, Idris’s more expressive type system leaves room for edge cases where blurring the line between type and implementation syntax could cause confusion. By separating the symbols early on, the language designers avoided potential parsing headaches down the line, especially as Idris evolved to support more advanced features like dependent pattern matching and implicit arguments.

Example Comparison #

To make this concrete, here’s how equivalent code looks in both languages:

Haskell:

add :: Int -> Int -> Int
add x y = x + y

double :: Int -> Int
double = \x -> add x x

describe :: Int -> String
describe n = case n of
  0 -> "Zero"
  1 -> "One"
  _ -> "Other"

Idris:

add : Int -> Int -> Int
add x y = x + y

double : Int -> Int
double = \x => add x x

describe : Int -> String
describe n = case n of
  0 => "Zero"
  1 => "One"
  _ => "Other"

In the Idris version, your eye immediately picks out which parts are type declarations (->) and which are implementation logic (=>)—no need to scan for \ or case keywords to orient yourself.

内容的提问来源于stack exchange，提问作者user9309163