Records and Classes

The source code for this module: PartI/Records.ard
The source code for the exercises: PartI/RecordsEx.ard

In this module we introduce very useful kinds of definitions: records and classes.

We also discuss the mechanism of coercions.

Records: \new, \cowith, projections, pattern matching

In the previous modules we saw two ways to arrange a sequence of types A1, …, An into a composite type of tuples: Sigma-types \Sigma A1 … An and data types \data Tuples | tuple A1 … An.

For example, a type of pairs of natural numbers can be defined as \Sigma Nat Nat. In this case elements of a pair x : \Sigma Nat Nat are accessed by means of projections x.1 and x.2. Alternatively, one can realize this type as a data type \data NatPair with projections defined by pattern matching:

\data NatPair | natPair Nat Nat

\func natFst (p : NatPair) : Nat
  | natPair x _ => x

\func natSnd (p : NatPair) : Nat
  | natPair _ y => y

The advantage of Sigma-type option is eta-equivalence: if x : \Sigma Nat Nat, then (x.1, x.2) == x, where == is computational equality. Eta-equivalence doesn’t hold for data types: natPair (natFst x) (natSnd x) is not computationally equal to x, one should prove that they are equal and use transport every time one wants to replace one with the other.

Record types provide the third option:

\record NatPair'
  | fst : Nat
  | snd : Nat

The major advantage of records over Sigma-types is that they allow to name components, which are called fields: we can write x.fst and x.snd instead of x.1 and x.2. And eta-equivalence also applies to elements of records.

Every field of a record is simply a function that has an instance of the record as its first implicit parameter:

-- fst : \Pi {x : NatPair'} -> Nat
\func foo (p : NatPair') => fst {p}

There is a namespace corresponding to a record, which contains all the fields of the record:

\func foo' (p : NatPair') => NatPair'.fst {p}

The syntax with dot p.snd can only be used to access fields if p is a variable and its type is specified explicitly:

\func bar (p : NatPair') => p.snd

-- (f x).snd -- This is not allowed. It can be replaced with one of the following variants:
-- \let e : NatPair' => f x \in e.snd
-- snd {f x}

-- This code will not typecheck since the type of p is not specified explicitly
-- \func baz {p p' : NatPair'} (q : p = p') => pmap (\lam p => p.fst) q

An element of a record can be created using the keyword \new:

\func zeroPair => \new NatPair' {
  | fst => 0
  | snd => 0
  }

Eta-equivalence for records, thus, means that \new NatPair’ { | fst => p.fst | snd => p.snd } is computationally equal to p:

\func etaNatPair' (p : NatPair') : p = \new NatPair' { | fst => p.fst | snd => p.snd }
  => idp

The pattern matching on variables of record types can be done using the same tuple patterns as used for pattern matching on variables of Sigma-types:

\func sum (p : NatPair') => fst {p} + p.snd

\func sum' (p : NatPair') : Nat
  | (a, b) => a + b

If we want to define a function that returns an element of a record, we can do this by means of copattern matching using the keyword \cowith:

-- This function is equivalent to zeroPair defined above.
-- \cowith is followed with a set of clauses, each starting
-- with | and specifying a field and its value
\func zeroPair' : NatPair' \cowith
  | fst => 0
  | snd => 0

Exercise 1: Define the function swap, which swaps components in pairs, in several ways: a) using \cowith and field access, b) using \new and pattern matching, c) using \new and field access.

Exercise 2: Prove that swap (swap p) = p.

Partial implementation

Given a record, it is possible to form new records out of it via partial implementation, that is by means of assigning values to some of its fields. If C is a record with fields f1, …, fn, then C { | f_{i_1} => e_{i_1} … | f_{i_k} => e_{i_k} } is a record formed by elements of the record C, where corresponding fields are implemented accordingly.

For example, NatPair’ { | fst => 0 } is the type of elements of the record NatPair’, whose first component is 0. This type is, thus, equivalent to the type Nat. We call such types anonymous extensions.

\func PartialEx : \Type => NatPair' { | fst => 0 }

\func ppp : NatPair' { | fst => 0 } => \new NatPair' { | snd => 1 }

Anonymous extensions of a record are subtypes of the record. If p is of type of the form C { … }, where the subset F of fields of C is implemented, then p is also of type of the form C { … }, where fields from a subset F’ of F are implemented and these implementations agree with the implementations in the former case. For example:

\func partial (p : NatPair' { | fst => 0 | snd => 1 }) : PartialEx => p

\func PartialEx' => NatPair' { | fst => 3 | snd => 7 }

The operator \new can be applied to any expression that evaluates to a record or its anonymous extension provided all fields are implemented. For example:

\func new => \new PartialEx'

Parameters, visibility of fields

Record types can have parameters:

\record Pair (A B : \Type)
  | fst : A
  | snd : B

Elements of such records can be created using \new or \cowith as before:

\func pairExample : Pair Nat (Nat -> Nat)
  => \new Pair { | fst => 1 | snd (x : Nat) => x }

Actually parameters of a record are also its fields. The example above can be equivalently rewritten as follows:

\func pairExample'
  => \new Pair { | A => Nat | B => Nat -> Nat | fst_ => 1 | snd_ (x : Nat) => x }

\func pairExample''
  => \new Pair Nat (Nat -> Nat) 1 (\lam (x : Nat) => x)

There is (almost) no difference between fields and parameters. In particular, it is perfectly fine to define all fields as parameters. For example, the following is an equivalent version of NatPair:

\record NatPair'' (fst'' snd'' : Nat)

\func natPair''ex => \new NatPair'' {
  | fst'' => 0
  | snd'' => 0
}

And, conversely, the type Pair has equivalent definition without parameters:

\record Pair'
  | A : \Type
  | B : \Type
  | fst : A
  | snd : B

Dependent records, a type of positive natural numbers

Records can be dependent, that is fields can depend on previous fields. This makes them fully equivalent to Sigma-types, the only difference is that components of a record are named.

For example, the set of positive natural numbers { n : Nat | T (isPos n) } can be expressed as Sigma-type \Sigma (n : Nat) (T (isPos n)) or as a record:

\data Bool | true | false

-- compare this definition of T with the one in module Basics
\data T (b : Bool) \with
  | true => tt

\func isPos (n : Nat) : Bool
  | 0 => false
  | suc _ => true

\record PosNat (n : Nat) (p : T (isPos n))

Exercise 3: Prove that the type PosNat 0 is empty, but the type PosNat 1 is not.

Exercise 4: Define the \record consisting of pairs of coprime natural numbers. Define the type of natural numbers that are coprime with 60.

Monoid

Another example of dependent records – the type of monoids. We define this type as a class using keyword \class instead of \record. Classes are very similar to records and almost equivalent to them. But there are some nice features that classes have and records don’t. We will discuss classes in more detail below.

\class Monoid (A : \Type)
  | id : A
  | \infixl 6 * : A -> A -> A
  | *-assoc (x y z : A) : (x * y) * z = x * (y * z)
  -- | *-assoc : \Pi (x y z : A) -> (x * y) * z = x * (y * z)
  | id-left (x : A) : id * x = x
  | id-right (x : A) : x * id = x

\func baz (m : Monoid Nat 0 (Nat.+)) => m.*-assoc

Classes and records can extend other records and classes. Some fields can be implemented in these extensions, this is useful when all instances of the extension are supposed to implement the field in the same way:

\class CommMonoid \extends Monoid
  | *-comm (x y : A) : x * y = y * x
  | id-right x => *-comm x id *> id-left x 
-- id-right follows from id-left for commutative monoids

We will discuss extensions in more detail below.

Classes, instances

The only difference between classes and records is that there is an instance inference mechanism available for classes. This mechanism is analogous to the one in Haskell.

Global instances of a class can be defined using \instance keyword. For example, there are two natural instances of the class Monoid for natural numbers: monoid on + and monoid on *.

\instance +-NatMonoid : Monoid Nat
  | id => 0
  | * => Nat.+
  | *-assoc => {?}
  | id-left => {?}
  | id-right => {?}

\instance *-NatMonoid : Monoid Nat
  | id => 1
  | * => Nat.*
  | *-assoc => {?}
  | id-left => {?}
  | id-right => {?}

-- alternative definition of the latter:
\instance *-NatMonoid' : Monoid Nat 1 (Nat.*) {?} {?} {?}

The first explicit parameter of a class is of special significance and is called classifying field of a class. The classifying field of a class is typically a carrier, on top of which all other fields of the class define some structure. Thus the type of the classifying field is often \Type or \Set. Classifying fields significantly affect the behavior of the instance inference algorithm. Basically, in case there are no local instances, the algorithm searches for a first appropriate global instance (appropriate in the sense that its classifying field coincides with some expected type).

Note, that the type of a class field is determined in the same way as in case of records. For example, for *:

* {M : Monoid} (x y : M.A) : M.A

Consider the following examples:

-- ok, +-NatMonoid is inferred since it was declared the first
-- id-left x here is equivalent to id-left {+-NatMonoid} x
\func +-test (x : Nat) : 0 Nat.+ x = x => id-left x
-- error, because +-NatMonoid is inferred, not *-NatMonoid
\func *-test (x : Nat) : 1 Nat.* x = x => id-left x

Such global instances behave like ordinary functions defined by copattern matching:

\func instEx => +-NatMonoid.id-left

\func instExF (M : Monoid) => M.id

\func instEx' => instExF +-NatMonoid

Arend classes can be used as typeclasses in Haskell. For example, Eq can be written as follows:

\class Eq (A : \Type)
  | \infix 3 == (x y : A) : Bool

-- function refl from Haskell can be defined in two ways
-- refl :: Eq a => a -> Bool
-- refl x = x == x
\func refl {A : \Type} {e : Eq A} (a : A) => a == a

\func refl' {E : Eq} (a : E) => a == a

-- \func xxxx => refl 1

Coercions

The classifying field of a class has a number of nice properties. For example, if in some place an element of type X is expected and X is the type of the classifying field of a class C, then any object of type C can be used in this place (the field accessor .X of the classifying field will be added implicitly).

In the following example M in the right-hand side of (x : M) is understood as M.A since an element of type \Type is expected:

\func CF-coerce (M : Monoid) (x : M) => x

This kind of substitutions are called coercions, we say that a class can be coerced to its classifying field. The mechanism of coercions in Arend allows also to define coercions between data types, classes and records. In order to be able to use elements of type A, where elements of type B are expected, one should define a function f : A -> B in the \where-block of either A or B as a coercion by using keywords \use \coerce. Elements a of type A will then be replaced with f a if they are used in a context, where B expected.

Consider the following example:

\data XXX | con

\data YYY | con' XXX Nat | con''
  \where {
    -- We can define coercions TO this type.
    -- The return type of the function must be YYY.
    \use \coerce fromXXX (x : XXX) => con' x 0
    
    -- We can also define coercions FROM this type.
    -- The type of the last parameter of the function must 
    -- be YYY.
    \use \coerce toXXX (y : YYY) => con
  }

\func fff (y : YYY) => y

-- Elements of type XXX are implicitly converted to type YYY by function fromXXX.
\func ggg => fff con

-- Implicit conversion from Nat to Int is done in this way:
\func hhh : Int => 0

Extensions, diamond problem

Records and classes can extend other classes. The list of records and classes extended by a given class can be specified after the keyword \extends as shown in the following example:

\record Base (A : \Type)

\record Base' (A : \Type)

\record X \extends Base
  | a : A

\record Y \extends Base'
  | b : A

\record Z \extends X, Y

\func zzz => \new Z {
  | A => {?}
  | a => {?}
  | Base'.A => {?}
  | b => {?}
  }

\func zzzz (z : Z) => Base'.A {z}

This means that the set of fields of a given class (or record) contains all fields declared in the class plus all the fields from the classes and records that it extends.

The record Z in the example above has four fields: Base.A, Base’.A, a and b. But if X and Y both extended the same record, say, Base, then Z would have had three fields:

\record X' \extends Base
  | aa : A

\record Y' \extends Base
  | bb : A

-- Z' has three fields: aa, bb, A
\record Z' \extends X', Y'

Consider an example from algebra: the type of rings. With a few simplifications, a possible definition might look as follows:

\class Monoid (A : \Type) {
  | \infixl 7 * : A -> A -> A
  | ide-left (x : A) : ide * x = x
  | ide-right (x : A) : x * ide = x
  | *-assoc (x y z : A) : (x * y) * z = x * (y * z)
}

\class CommMonoid \extends Monoid {
  | comm (x y : A) : x * y = y * x
  | ide-right x => comm x ide *> ide-left x
}

\class AbGroup \extends CommMonoid {
  | inverse : A -> A
  | inv-left (x : A) : inverse x * x = id
  | inv-right (x : A) : x * inverse x = id
}

-- We omit distributivity
\class Ring \extends AbGroup
  | mulMonoid : Monoid A

In order to distinguish the structure of addition from the structure of multiplication we do not extend Monoid, but add it as a field instead. Note that we explicitly specify the underlying classifying field of mulMonoid so that it matches with the carrier of the ring’s additive group structure.

If we try to define the type of rings that extends class AbGroup for the abelian group of addition and class Monoid for the monoid of multiplication, we will get into trouble: the clash of two monoidal structures. This is called the diamond problem.

-- This is not a correct way to define the class Ring:
-- the structures of addition and multiplication coincide.
\class Ring \extends AbGroup, Monoid

A possible way to make it work is to define another copy of AbGroup that does not extend Monoid:

-- This class does not extend Monoid
\class AbGroup' (A : \Type) {
  -- Here all the fields of Monoid, CommMonoid and AbGroup 
  -- should be repeated
}

\class Ring' \extends AbGroup', Monoid
  | Monoid.A => AbGroup'.A -- make sure that classifying fields coincide

This approach is adopted in Arend standard library with one small improvement: algebraic structures extend the same BaseSet class in order to avoid identifications such as Monoid.A => AbGroup’.A above.

Definitions inside classes

It is possible to define functions and data structures inside classes. For example, we can modify the definition of a ring as follows:

\class Ring {
  ...

  \func two => ide + ide
  \func square (x : A) => x * x
}

Note that functions are defined inside the class (not in its \where block). The system adds one implicit parameter of type Ring to such functions. Thus, the definition above is equivalent to the following:

\class Ring {
  ...
} \where {
  \func two {this : Ring} => ide + ide
  \func square {this : Ring} (x : A) => x * x
}

Classes without classifying fields

It is often necessary to have a group of functions with a common set of parameters. For example, consider the following snippet that defines injective, surjective, and bijective functions and proves their properties:

-- Implementations are omitted

\func isInj {A B : \Type} (f : A -> B) : \Type => {?}

\func isSur {A B : \Type} (f : A -> B) : \Type => {?}

\func isBij {A B : \Type} (f : A -> B) : \Type => {?}

\func IsInj+isSur=>isBij {A B : \Type} (f : A -> B) (p : isInj f) (q : isInj f) : isBij f => {?}

\func IsBij=>isInj {A B : \Type} (f : A -> B) (p : isBij f) : isInj f => {?}

\func IsBij=>isSur {A B : \Type} (f : A -> B) (p : isBij f) : isSur f => {?}

Functions above have 3 common parameters: A, B, and f. Classes without classifying fields can be used to extract these parameters so that we do not have to type in them for every function. A class without classifying fields can be defined in two ways: as a class without explicit parameters, or as a class with the keyword \noclassifying.

The example above can be rewritten as follows:

\class Map \noclassifying {A B : \Type} (f : A -> B) {
  \func isInj : \Type => {?}

  \func isSur : \Type => {?}

  \func isBij : \Type => {?}

  \func isInj+isSur=>isBij (p : isInj) (q : isInj) : isBij => {?}

  \func isBij=>isInj (p : isBij) : isInj => {?}

  \func isBij=>isSur (p : isBij) : isSur => {?}
}

Since Map is a class without classifying fields, the system will infer the first available instance of this class whenever one the functions above is invoked:

\func isInj+isSur<=>isBij (m : Map) : \Sigma (isBij -> \Sigma isInj isSur) (\Sigma isInj isSur -> isBij)
  => ((\lam p => (isBij=>isInj p, isBij=>isInj p)), (\lam p => isInj+isSur=>isBij p.1 p.2))
  \where \open Map

Of course, a function from the class Map can also be invoked with an explicitly specified instance:

\func id-isInj {A : \Type} : Map.isInj {\new Map (\lam (a : A) => a)} => {?}

Of course, classes without classifying fields can also be extended. For example, if we want to define a few functions about endomorphisms, we can extend the class Map as follows:

\class Endo \extends Map {
  | B => A

  \func isIdem => \Pi (x : A) -> f (f x) = f x

  \func isInv => \Pi (x : A) -> f (f x) = x

  \func isIdem+isInv=>id (p : isIdem) (q : isInv) : f = (\lam x => x) => {?}
}

Functor

We conclude by demonstrating another example: the class of functors.

\class Functor (F : \Type -> \Type)
  | fmap {A B : \Type} (f : A -> B) : F A -> F B
  | fmap-id {A : \Type} (y : F A) : fmap (\lam (x : A) => x) y = y
  | fmap-comp {A B C : \Type} (f : A -> B) (g : B -> C) (y : F A)
    : fmap (\lam x => g (f x)) y = fmap g (fmap f y)

Exercise 5: Define the class of monads, which extends the class of functors Functor. Define \instance of this class for Maybe.

Exercise 6: Define instances for the class of monads for State and State’.

\record State (S A : \Type)
  | state : S -> \Sigma S A

\data State' (S A : \Type)
  | state' (S -> \Sigma S A)