This is the main embedding of Fortran types. A value of type D a represents the Fortran type which corresponds to the Haskell type a. a is a phantom type parameter. There is at most one instance of D a for each a. This means that a value of type D a acts as a kind of proof that it possible to have a Fortran type corresponding to the Haskell type a -- and that when you match on D a knowing the particular a you have, you know which constructor you will get. This is a nice property because it means that GHC (with -fwarn-incomplete-patterns) will not warn when you match on an impossible case. It eliminates situations where you'd otherwise write error "impossible: ...".

• DPrim p :: D (PrimS a) is for primitive types. It contains a value p of type Prim p k a for some p, k, a. When matching on something of type D (PrimS a), you know it can only contain a primitive type.
• DArray i v :: D (Array i v) is for arrays. It contains instances of Index i and ArrValue a. Index i is a proof that i can be used as an index, and ArrValue a is a proof that a can be stored in arrays.
• DData s xs :: D (Record name fs) is for user-defined data types. The type has a name, represented at the type level by the type parameter name of kind Symbol. The constructor contains s :: SSymbol name, which acts as a sort of value-level representation of the name. SSymbol is from the singletons library. It also contains xs :: Rec (Field D) fs. fs is a type-level list of pairs, pairing field names with field types. Field D '(fname, b) is a value-level pair of SSymbol fname and D b. The vinyl record is a list of fields, one for each pair in fs.

This newtype wrapper is used in DPrim for semantic primitive types. This means that when matching on something of type D (PrimS a), we know it can't be an array or a record.

Lists the allowed primitive Fortran types. For example, PInt8 :: Prim 'P8 'BTInt Int8 represents 8-bit integers. Prim has three phantom type parameters: precision, base type and semantic Haskell type. Precision is the number of bits used to store values of that type. The base type represents the corresponding Fortran base type, e.g. integer or real. Constructors are only provided for those Fortran types which are semantically valid, so for example no constructor is provided for a 16-bit real. A value of type Prim p k a can be seen as a proof that there is some Fortran primitive type with those parameters.

Specifies which types can be used as array indices.

Specifies which types can be stored in arrays. Currently arrays of arrays are not supported.

An array with a phantom index type. Mostly used at the type-level to constrain instances of D (Array i a) etc.

A field over a pair of name and value type.

A type of records with the given name and fields. Mostly used at the type level to constrain instances of D (Record name fields) etc.

Any Fortran index type is a valid Fortran type.

Anything that can be stored in Fortran arrays is a valid Fortran type.

Given a field with known contents, we can change the functor and value type.

Given a field with unknown contents, we can change the functor but not the value type.

Combine two fields over the same name-value pair but (potentially) different functors.