So far in our story all of our types, and programs, we have worked with require specifications that work with specific datatypes.
Generic types are ones that can work with others.
We have seen such types before:
list in Python,
and
seq in Dafny
These two types,
however,
are primitives.
Idris’ List is not!
Yet the operations for these sequence types work with sequences that contain different types.
In this topic, we will look at how we can write generic programs that use generic datatypes.
You may have heard the term polymorphism used to describe generic types. With monomophism, describing types that are not generic. Polymorphism refers to more mathematically structured approaches to making data types generic.
Specifically, we will look at:
- generic datatypes, how we can generalise datatypes to work with different types of value;
- generic methods/functions, how we can make programs that work with many types;
- higher-order programs, how we can make programs that work work with other programs;
Learning Outcomes
By the end of this topic, for each language, you will:
- understand how one can write generic datatypes;
- know how to write generic programs;
- know how to write higher-order programs;