Idris是否支持row-polymorphism？如何构造类PureScript的异构匿名记录？

Great questions! Let's break this down clearly, since these are core parts of Idris's type system and record handling.

Absolutely—row polymorphism is a first-class feature in Idris, baked directly into its record and type system. This is how Idris enables functions to work with records that have a subset of required fields, regardless of other extra fields they might contain.

For example, here's a function that can greet any record with a name : String field, no matter what other fields the record has:

greet : {auto prf : HasField "name" r String} -> r -> String
greet rec = "Hello, " ++ getField "name" rec

-- Works with a record that has just a name
person1 : { name : String }
person1 = { name = "Bob" }
test1 : String
test1 = greet person1 -- Returns "Hello, Bob"

-- Also works with a record that has extra fields
person2 : { name : String, age : Int, city : String }
person2 = { name = "Alice", age = 30, city = "London" }
test2 : String
test2 = greet person2 -- Also returns "Hello, Alice"

The HasField "name" r String constraint tells the compiler: "r must be a record type that includes a field named name with type String". This is pure row polymorphism—our function doesn't care about the rest of the record's structure, only the specific field it needs.

Idris has robust support for anonymous, heterogenous records with compile-time type checking that matches what you're describing in PureScript. Here's how to work with them:

1. Create an anonymous heterogeneous record #

Use curly braces with key-value pairs—each field can have a different type, and the compiler infers the row type automatically:

-- The compiler infers this as { name : String, age : Int, isStudent : Bool }
basicRec = { name = "Charlie", age = 22, isStudent = True }

2. Append fields (extend the record) #

Use the <+> operator to merge two records, which effectively appends new fields (the compiler will throw an error if you try to duplicate field names):

-- Extend with a new field `gpa : Double`
extendedRec = basicRec <+> { gpa = 3.8 }
-- Now extendedRec has type { name : String, age : Int, isStudent : Bool, gpa : Double }

3. Modify existing fields #

Use the record { field = newValue } syntax to create a new record with an updated field. The compiler ensures you're assigning a value of the correct type to an existing field:

-- Update the age field to 23
updatedRec = record { age = 23 } basicRec

-- This will fail at compile time: age expects an Int, not a String
-- badUpdate = record { age = "twenty-three" } basicRec

4. Type-safe field access #

Use getField to access fields, and the compiler will verify both that the field exists and that you're using it with the correct type:

studentStatus : Bool
studentStatus = getField "isStudent" basicRec -- Compiles fine

-- This will fail: no "height" field exists in basicRec
-- badAccess = getField "height" basicRec

Key note on immutability #

Like most functional languages, Idris records are immutable—"editing" or "modifying" actually creates a new record with the desired changes. This is consistent with PureScript's behavior, and it ensures type safety throughout your code.

The compiler will always enforce that any code consuming a record uses fields with the correct types. If a function expects a record with age : Int, passing a record where age is a String (or missing entirely) will result in a compile-time error, just like in PureScript.

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