@@ -1021,3 +1021,89 @@ value of the same type.
1021determined \emph{without} type checking the \texttt{case}-expression itself.
1021determined \emph{without} type checking the \texttt{case}-expression itself.
1022\end{itemize}
1022\end{itemize}
1024+\subsection{Dependent Records}
1026+\remph{Records} are data types which collect several values (the record's
1027+\remph{fields}) together. \Idris{} provides syntax for defining records and
1028+automatically generating field access and update functions. For example, we
1029+can represent a person's name and age in a record:
1031+\begin{SaveVerbatim}{recsimpl}
1033+record Person : Set where
1034+ MkPerson : (name : String) ->
1035+ (age : Int) -> Person
1038+fred = MkPerson "Fred" 30
1044+Record declarations are like \texttt{data} declarations, except that they are
1045+introduced by the \texttt{record} keyword, and can only have one constructor.
1046+The names of the binders in the constructor type (\texttt{name} and \texttt{age})
1047+here are the field names, which we can use to access the field values:
1049+\begin{SaveVerbatim}{recaccess}
1056+name : Person -> String
1062+We can also use the field names to update a record (or, more precisely, produce a
1063+new record with the given fields updates).
1065+\begin{SaveVerbatim}{recupdate}
1067+*record> record { name = "Jim" } fred
1068+MkPerson "Jim" 30 : Person
1069+*record> record { name = "Jim", age = 20 } fred
1070+MkPerson "Jim" 20 : Person
1076+The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1077+the given fields in a record.
1079+Records, and fields within records, can have dependent types.
1080+Updates are allowed to change the type of a field,
1081+provided that the result is well-typed, and the result does not affect the type of
1082+the record as a whole. For example:
1084+\begin{SaveVerbatim}{deprec}
1086+record Class : Set where
1087+ ClassInfo : (students : Vect Person n) ->
1088+ (className : String) ->
1095+It is safe to update the \texttt{students} field to a vector of a different length
1096+because it will not affect the type of the record:
1098+\begin{SaveVerbatim}{addstu}
1100+addStudent : Person -> Class -> Class
1101+addStudent p c = record { students = p :: students c } c
1103+*record> addStudent fred (ClassInfo [] "CS")
1104+ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"