Idris中为何接口参数必须是类型或数据构造器？

Let's break down why you ran into that error, and how to work around it while keeping your algebraic structure definitions clean.

Why the Error Happens #

First, let's clarify the core issue: even though Idris blurs lines between values, types, and kinds, interface (type class) instances are indexed by types, not arbitrary values.

When you tried to define Group with op, e, and inv as parameters, Idris rejected it because those are value-level entities (functions, constants), not types or data constructors. The instance resolution system in Idris needs a way to uniquely look up instances based on type information alone. If you allowed a function like (+) as an interface parameter, the type checker couldn't distinguish between two instances for the same G but different operations—for example, Group Nat (+) Z negate and Group Nat (*) 1 recip would both have Nat as their first parameter, and Idris has no way to pick the right one automatically.

In short: interface parameters must be things the type checker can use as a "key" for instance lookup, and values (like functions) don't qualify for that role.

How to Model Algebraic Structures in Idris #

You have two main approaches to handle this, depending on whether you want to use interfaces (for implicit instance lookup) or explicit structure records (for full flexibility with multiple structures on the same type).

Approach 1: Use Newtypes to Encode Operation Context #

Wrap your base type in a "marker" newtype that encodes the algebraic operation (like additive vs multiplicative). This lets you define separate interface instances for each wrapped type, even if they're based on the same underlying set.

Here's how you'd redefine Group and its instances:

interface Group a where
  op : a -> a -> a
  e : a
  inv : a -> a
  assoc : {x,y,z : a} -> op (op x y) z = op x (op y z)
  id_l : {x : a} -> op x e = x
  id_r : {x : a} -> op e x = x
  inv_l : {x : a} -> op x (inv x) = e
  inv_r : {x : a} -> op (inv x) x = e

-- Newtype for additive groups
newtype Additive a = Add a

instance Num a => Group (Additive a) where
  op (Add x) (Add y) = Add (x + y)
  e = Add 0
  inv (Add x) = Add (-x)
  assoc = Refl
  id_l = Refl
  id_r = Refl
  inv_l = Refl
  inv_r = Refl

-- Newtype for multiplicative groups (requires fractional support)
newtype Multiplicative a = Mult a

instance Fractional a => Group (Multiplicative a) where
  op (Mult x) (Mult y) = Mult (x * y)
  e = Mult 1
  inv (Mult x) = Mult (recip x)
  assoc = Refl
  id_l = Refl
  id_r = Refl
  inv_l = Refl
  inv_r = Refl

This works because Additive Nat and Multiplicative Nat are distinct types, so Idris can resolve the correct Group instance based on the type being used.

Approach 2: Use Dependent Records for Explicit Structures #

If you prefer a style closer to your original idea (directly bundling the set, operations, and axioms), use a dependent record type instead of an interface. This lets you create multiple structure instances for the same base type without newtypes, since you'll pass the record explicitly rather than relying on implicit instance lookup.

Example:

record GroupRecord where
  constructor MkGroup
  G : Type
  op : G -> G -> G
  e : G
  inv : G -> G
  assoc : {x,y,z : G} -> op (op x y) z = op x (op y z)
  id_l : {x : G} -> op x e = x
  id_r : {x : G} -> op e x = x
  inv_l : {x : G} -> op x (inv x) = e
  inv_r : {x : G} -> op (inv x) x = e

-- Integer additive group
intAddGroup : GroupRecord
intAddGroup = MkGroup
  G = Int
  op = (+)
  e = 0
  inv = negate
  assoc = Refl
  id_l = Refl
  id_r = Refl
  inv_l = Refl
  inv_r = Refl

-- Non-zero integer multiplicative group (simplified)
intMultGroup : GroupRecord
intMultGroup = MkGroup
  G = Int
  op = (*)
  e = 1
  inv = \x => if x == 0 then 0 else recip x
  assoc = Refl
  id_l = Refl
  id_r = Refl
  inv_l = Refl
  inv_r = Refl

This approach is more flexible for cases where you need to work with multiple structures on the same type, but you'll have to pass the GroupRecord explicitly to functions that need it, rather than relying on implicit interface constraints.

Handling Semirings (Your Follow-Up Concern) #

For semirings (which require two monoids: additive and multiplicative), you can combine these approaches. Define a Semiring interface that depends on two Monoid instances (using newtypes for additive/multiplicative contexts), or create a dependent record that bundles both monoid structures plus the distributive laws.

Example interface-based semiring:

interface Monoid a where
  m_op : a -> a -> a
  m_e : a
  m_assoc : {x,y,z : a} -> m_op (m_op x y) z = m_op x (m_op y z)
  m_id_l : {x : a} -> m_op x m_e = x
  m_id_r : {x : a} -> m_op m_e x = x

interface (Monoid (Additive a), Monoid (Multiplicative a)) => Semiring a where
  distribute_l : {x,y,z : a} -> x * (y + z) = (x * y) + (x * z)
  distribute_r : {x,y,z : a} -> (x + y) * z = (x * z) + (y * z)

instance Semiring Int where
  distribute_l = Refl
  distribute_r = Refl

This reuses the additive/multiplicative newtypes to get the two monoid instances, avoiding redundant code.

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