Basic idea of using singleton types like Nat n where n is a value from the index domain, to connect program expressions and index expressions.\xa0 The data value of type Nat n is a copy of n, but living in the syntactic category of program expressions.\xa0 This allows programs to operate on a proxy for n.\xa0 Singletons library in Haskell mentioned.