Programming with Indexed Types

Published: Jan. 13, 2020, 11 p.m.

Indexed datatypes like vectors, where the indices come from a different syntactic category than program expressions.