@@ -1021,3 +1021,89 @@ value of the same type.
10211021determined \emph{without} type checking the \texttt{case}-expression itself.
10221022\end{itemize}
10231023
1024+\subsection{Dependent Records}
1025+
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:
1030+
1031+\begin{SaveVerbatim}{recsimpl}
1032+
1033+record Person : Set where
1034+ MkPerson : (name : String) ->
1035+ (age : Int) -> Person
1036+
1037+fred : Person
1038+fred = MkPerson "Fred" 30
1039+
1040+\end{SaveVerbatim}
1041+\useverb{recsimpl}
1042+
1043+\noindent
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:
1048+
1049+\begin{SaveVerbatim}{recaccess}
1050+
1051+*record> name fred
1052+"Fred" : String
1053+*record> age fred
1054+30 : Int
1055+*record> :t name
1056+name : Person -> String
1057+
1058+\end{SaveVerbatim}
1059+\useverb{recaccess}
1060+
1061+\noindent
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).
1064+
1065+\begin{SaveVerbatim}{recupdate}
1066+
1067+*record> record { name = "Jim" } fred
1068+MkPerson "Jim" 30 : Person
1069+*record> record { name = "Jim", age = 20 } fred
1070+MkPerson "Jim" 20 : Person
1071+
1072+\end{SaveVerbatim}
1073+\useverb{recupdate}
1074+
1075+\noindent
1076+The syntax \texttt{record \{ field = val, ... \}} generates a function which updates
1077+the given fields in a record.
1078+
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:
1083+
1084+\begin{SaveVerbatim}{deprec}
1085+
1086+record Class : Set where
1087+ ClassInfo : (students : Vect Person n) ->
1088+ (className : String) ->
1089+ Class
1090+
1091+\end{SaveVerbatim}
1092+\useverb{deprec}
1093+
1094+\noindent
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:
1097+
1098+\begin{SaveVerbatim}{addstu}
1099+
1100+addStudent : Person -> Class -> Class
1101+addStudent p c = record { students = p :: students c } c
1102+
1103+*record> addStudent fred (ClassInfo [] "CS")
1104+ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1105+ : Class
1106+
1107+\end{SaveVerbatim}
1108+\useverb{addstu}
1109+