Support for row types

[wintermute-motherbrain]

Currently it seems its not possible to have structured types (e.g. records). Are there any plans to add support for row algebra? If not, any guidance for if one wanted to extend the library to support it?

Thanks!

[wintermute-motherbrain]

I was able to modify the library to support it, not sure I did it the proper way but thought I'd share.

Modification to Type enum in types.rs

pub enum Type<N: Name = &'static str> {
    Constructed(N, Vec<Type<N>>),
    Variable(Variable),
    Row(Vec<(N, Type<N>)>, Option<Box<Type<N>>>),  // new
    RowVariable(Variable),  // new
}

Modification to unify_inner() in context.rs

fn unify_internal(&mut self, t1: Type<N>, t2: Type<N>) -> Result<(), UnificationError<N>> {
    if t1 == t2 {
        return Ok(());
    }
    match (t1, t2) {
        // .....
        // .....
        // added code:
        (Type::Row(mut fields1, tail1), Type::Row(mut fields2, tail2)) => {
                let mut remaining_fields1 = vec![];
                let mut remaining_fields2 = vec![];
                let mut matched_fiels = 0;
            
                // Match common fields
                for (name1, typ1) in fields1.drain(..) {
                    if let Some((index, (_, typ2))) = fields2
                        .iter()
                        .enumerate()
                        .find(|(_, (name2, _))| name2 == &name1)
                    {
                        // Use typ2 directly for unification
                        self.unify_internal(typ1, typ2.clone())?;
                        fields2.remove(index); // Remove the matched field from fields2
                        matched_fiels += 1;
                    } else {
                        remaining_fields1.push((name1, typ1));
                    }
                }
                remaining_fields2.extend(fields2);
            
                // Handle tails
                match (tail1, tail2) {
                    (Some(t1), Some(t2)) => {
                        if matched_fiels == 0 {
                            self.unify_internal(*t1, *t2)?;
                        } else {
                            let extended_row1 = Type::Row(remaining_fields1, Some(t1));
                            let extended_row2 = Type::Row(remaining_fields2, Some(t2));
                            self.unify_internal(extended_row1, extended_row2)?;
                        }
                    }
                    (Some(t1), None) => {
                        // Open row t1 must absorb remaining fields of the closed row
                        if !remaining_fields1.is_empty() {
                            return Err(UnificationError::Failure(
                                Type::Row(remaining_fields1, Some(t1.clone())),
                                Type::Row(remaining_fields2, None),
                            ));
                        }
                        let extended_row = Type::Row(remaining_fields2, None);
                        self.unify_internal(*t1, extended_row)?;
                    }
                    (None, Some(t2)) => {
                        // Open row t2 must absorb remaining fields of the closed row
                        if !remaining_fields2.is_empty() {
                            return Err(UnificationError::Failure(
                                Type::Row(remaining_fields1, None),
                                Type::Row(remaining_fields2, Some(t2.clone())),
                            ));
                        }
                        let extended_row = Type::Row(remaining_fields1, None);
                        self.unify_internal(*t2, extended_row)?;
                    }
                    (None, None) => {
                        // Both rows are closed; ensure no extra fields remain
                        if !remaining_fields1.is_empty() || !remaining_fields2.is_empty() {
                            return Err(UnificationError::Failure(
                                Type::Row(remaining_fields1, None),
                                Type::Row(remaining_fields2, None),
                            ));
                        }
                    }
                }
            
                Ok(())
            }
            (Type::RowVariable(v), t2) | (t2, Type::RowVariable(v)) => {
                if t2.occurs(v) {
                    Err(UnificationError::Occurs(v))
                } else {
                    self.extend(v, t2);
                    Ok(())
                }
            }
            (t1, t2) => Err(UnificationError::Failure(t1, t2)),
    }
}

The remaining changes were trivial (e.g. show, occurs, etc)