From f36a3866e5dd826d07c43e2ac0716577c597f292 Mon Sep 17 00:00:00 2001 From: Noel Welsh Date: Tue, 17 Dec 2024 08:28:55 +0000 Subject: [PATCH] A bit more on indexed data --- src/pages/indexed-types/data.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/pages/indexed-types/data.md b/src/pages/indexed-types/data.md index ff9dfdbf..29795965 100644 --- a/src/pages/indexed-types/data.md +++ b/src/pages/indexed-types/data.md @@ -1,3 +1,20 @@ ## Indexed Data The key idea of indexed data is to encode type equalities in data. +When we come to inspect the data (usually, via structural recursion) we discover these equalities, which in turn limit what values we can produce. +Notice, again, the duality with codata. +Indexed codata limits methods we can call. +Indexed data limits values we can produce. +Also, remember that indexed data is often known as generalized algebraic data types. +We are using the simpler term indexed data to emphasise the relationship to indexed codata, +and also because it's much easier to type! + +Let's see a simple, and classic, example: evaluating a small language. +Our language will have basic arithmetic as well as conditionals, which is just enough to make it interesting. +We'll start with the version without indexed data. + +```scala mdoc:silent +enum Expr { + case +} +```