无参数类型构造函数引发‘Can't infer argument’错误：Haskell与Idris差异解析

The core issue here boils down to key differences in how Haskell and Idris handle type inference and polymorphism, especially for parameterized data constructors. Let's break this down clearly:

1. How Haskell handles Empty #

In Haskell, your definition data MyList a = Empty | Cons a (MyList a) makes Empty a polymorphic value with the type MyList a (or more explicitly, forall a. MyList a).

Haskell's type inference is built to be permissive with unconstrained polymorphism:

• When you write Empty without any surrounding context, Haskell infers its type as the fully polymorphic forall a. MyList a.
• The compiler accepts this "floating" polymorphic value because Haskell's type system (by default) supports implicit universal quantification for top-level expressions and bindings. Even in GHCi, typing Empty will return its polymorphic type without complaint.

2. Why Idris rejects Empty #

Idris is a strict, explicitly typed dependently typed language that prioritizes type clarity and eliminates ambiguity wherever possible. Here's why it throws the error:

• The Empty constructor still has a type parameter a, but Idris requires all type parameters to be either:
  • Explicitly specified (e.g., Empty {a = Int} or Empty :: MyList String), or
  • Inferable from the immediate context where Empty is used.
• When you write Empty in isolation (with no context hinting at what a should be), Idris has no way to resolve the concrete type for a. Unlike Haskell, it won't default to a polymorphic forall a. MyList a for standalone expressions—Idris expects every expression to have a concrete, resolvable type.

Fixing the error in Idris #

To use Empty without errors in Idris, you have straightforward options:

• Explicitly annotate the type:

  emptyStringList : MyList String
  emptyStringList = Empty
  

• Specify the type parameter directly via named arguments:

  Empty {a = Bool}
  

• Or use it in a context where the type is clear (e.g., passing it to a function that expects a MyList Int).

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