 Most dependently typed proof assistants and later dependently typed languages such as Agda included a termination checker to prevent the type checker from looping, while the contemporary Dependent ML restricted the expressivity of the type-level language to maintain decidability.There are very few building blocks in the language, but much syntactic sugar to make it more readable.The basic types are functions, products, and sums.