Any, All, and the Hidden Power of lolnogenerics

This is going to sound really odd, especially if you have have some passing familiarly with Idris, but Idris doesn't actually have generics. Sure, it has something that looks like generics, and can do everything generics can do, but it isn't actually generics, at least not in terms of the usual conceptual framework programmers have for generics. What Idris actually has is something more fundamental, in a sense simpler than generics, yet infinitely more flexible.

But These Really Look Like Generics

Lets consider an example, map, the function that applies another function to each element in some arbitrary collection. For our purposes, lets say it has the following type signature:

map1 : Functor t => (f : a -> b) -> (xs : t a) -> t b

And if you are thinking this sure looks like it has generics, you would be right. This function certainly appears to be generic over the types a and b, as well as any type t that implements Functor, and by extension the type of the function f. But do not let "looks like" fool you. The layers of sugar present in Idris create an illusion, and things are not quite what they seem.

Getting to The Center of a Tootsie Pop

The => syntax, usually used to bound a type such that it implements an interface, is actually just syntactic sugar, decomposing into an auto-implicit argument. We can rewrite map as follows without changing it's meaning:

map2 : {auto functor_impl : Functor t} -> (f : a -> b) -> (xs : t a) -> t b

The implicit binding that happens when an unbound lowercase argument appears, such as the a, b, and t in this function's signature, is yet more sugar. They all get lifted into their own implicit arguments¹. Let's rewrite map again to take this into account:

map3 : {a : Type} -> {b : Type} -> {t : Type -> Type} -> {auto functor_impl : Functor t}
  -> (f : a -> b) -> (xs : t a) -> t b

auto-implicits are another fiction, getting filled in during elaboration. Reducing them out, we get:

map4 : {a : Type} -> {b : Type} -> {t : Type -> Type} -> {functor_impl : Functor t}
  -> (f : a -> b) -> (xs : t a) -> t b

We can check that we are on the right track by inspecting the standard library's map function at the REPL:

Prelude.map : {0 b : Type} -> {0 a : Type} -> {0 f : Type -> Type} -> Functor f =>
(a -> b) -> f a -> f b

Implicits themselves are yet another sweet fantasy, the barest core of Idris does not have them, they get converted into explicit arguments during the lowering process, before type checking completes. In the lowest level core language, map looks more like this:

map5 : (a : Type) -> (b : Type) -> (t : Type -> Type) -> (functor_impl : Functor t)
  -> (f : a -> b) -> (xs : t a) -> t b

Translating to Another Language

To try and gain a sense of perspective, lets translate our fully lowered map into a Rust function signature. To allow us to ignore Rust's lack of higher kinded types², and make it a bit less of a mouthful, we'll ignore the polymorphism over Functor, and manually monomorphize it over List. Otherwise, we'll do a direct translation without regard for the limitations of Rust's type system, and clean it up in the next step:

fn map(A: Type, B: Type, f: Fn(A) -> B, xs: List<A>) -> List<B> { ... }

Wait, uh, huh... Ignoring for a second that this would never work as written, because types aren't values in Rust and Rust evaluates function signatures "all at once" so to speak, not allowing for dependency between arguments, this function signature... doesn't have any generics, at least not in the sense of Rust's generics.

Unlowering

We are going to have to perform some modifications to the Rust version for it to actually work in Rust's type system. We'll ignore the whole "family of function interfaces" situation, since it's not salient to the point of this article. After extracting our type arguments into generics we are left with:

fn map<A, B>(f : Fn(A) -> B, xs: List<A>) -> List<B> {...}

If you squint a bit, its almost like the type arguments are still regular arguments, just lifted into ~special~ ones that don't quite play by the same rules. As with any time you insert an object that's almost like one of the fundamental objects, but ~special~, into a system, this comes with the addition of all sorts of arbitrary restrictions. Rust's generics are heavily restricted compared to normal arguments, and extremely heavily restricted compared to the dependently typed version.

Approaching from the dependently typed direction, slowly reducing the Idris version of map into its Rust equivalent, it becomes clear that it's appropriate to think of the-thing-Idris-has as the more fundamental concept, and Rust's generics as a restricted subset. On the dependently typed side, instead of "generics" existing as their own first class construct in the type system, they show up as a specific invocation of a more general aspect of the system, just another case of types depending on values. Only, in this instance, the values being depended on are themselves types.

This deeper integration into the overall type system often simplifies the logical burden of dealing with complex structures, and comes with numerous other benefits, placing many useful magic tricks at our disposal.

Another Angle

We've gotten a pretty good idea of how the-thing-that-Idris-has compares to Rust's generics, but we are still missing some insights about it from the Idris side. Lets jump to the least complicated function we can find and consider the identity function:

id : a -> a
id x = x

If we query it's debugging information at the REPL:

DependentNuggets.AnyAllLolnogenerics.id
Arguments [{arg:0}, {arg:1}]
Compile time tree: {arg:1}
Erasable args: [0]
Inferrable args: [0]
Compiled: \ {arg:1} => {arg:1}
Flags: inline, total

It tells us that our id function has two arguments, the first of which is both erasable, meaning it doesn't have to exist at runtime, and inferable, meaning it can be forced to take on a particular value by type checking alone. This is a bit odd, we only wrote id with one argument.

Let's try applying a round of our desugaring rules from above to see if we can figure out what's going on:

id' : {0 a : Type} -> a -> a
id' x = x

Running :di on this again, we can see we are on the right track:

DependentNuggets.AnyAllLolnogenerics.id'
Arguments [{arg:0}, {arg:1}]
Compile time tree: {arg:1}
Erasable args: [0]
Inferrable args: [0]
Compiled: \ {arg:1} => {arg:1}
Flags: inline, total

So we now know that {0 a : Type} -> a -> a is the actual type signature of id. While one could look at this as a function that's generic over types, there is a much more interesting interpretation: id is a function from a type a to the monomorphic/non-generic identity function for values of a.

Things get even more interesting if we un-erase the type argument, we can then pattern match over the type, and make practical use of this "function from a type to another function" concept in a way that Rust programmers might recognize as similar to specialization:

reallyFunnyId : {a : Type} -> a -> a
reallyFunnyId {a = String} = const "This is most likely not the string given as input"
reallyFunnyId {a = Nat} = (+ 1)
reallyFunnyId {a} = \x => x

Interfaces

Before addressing some of the more advanced type-level programming concepts in this article, it will be helpful to develop an understanding of how interfaces work in Idris. At first glance, interfaces in Idris are quite similar to traits in Rust, with a few notable differences. Importantly, you can implement the same Idris interface for the same type multiple times, and implementations can be given individual names allowing the programmer to disambiguate when needed, eliminating the need for an equivalent to the orphan rule³. And yes, this does mean that package A can implement package B's interfaces for types in package C without issue in Idris.

Breaking Down an Interface Bound

When we implement a function that's polymorphic over an interface in Idris, we generally default to using the => syntax. Consider this example function:

greet : Show t => (x : t) -> String
greet x = "Hello \{show x}"

As previously discussed, the => argument desugars into an auto-implicit, like so:

greet' : {auto _ : Show t} -> (x : t) -> String
greet' x = "Hello \{show x}"

So our greet function, which is polymorphic over any type t implementing the Show interface, is actually a function that accepts a value of Show t and returns a function from a value of type t to a String. That's all well and good, but what is this Show t type, and what do values of type Show t look like?

Constructive Witness

For any given interface I, a value of type I t serves as a witness that the type t implements the interface I. This isn't some highly abstract forgetful witness though, it's a constructive witness, proving the implementation by providing the implementing functions for each of the interface methods.

This is quite similar to the concept of a vtable, or a trait object in Rust⁴. If we take a look at the type of a bare interface method, such as show from Show:

Prelude.show : Show ty => ty -> String

We see that the interface method itself accepts the implementation witness as an auto-implicit, and it uses that witness to dispatch to the corresponding method from the provided implementation.

Named Implementations

Since interfaces in Idris are passed into functions as normal arguments, the language has no issues with the same interface being implemented for the same type multiple times, as only one can ever be passed in through single argument at a time. Idris allows us to give names to specific implementations, in square brackets ([]) before the implementation, allowing the programmer to disambiguate when needed, like so:

[funnyShow]
Show String where
  show _ = "Ha Ha, stole your string!"

This name, funnyShow, is a normal first class value. Since this is an implementation of Show for String, we might expect that this value has type Show String, inspecting the type at the REPL, we see that is the case:

DependentNuggets.AnyAllLolnogenerics.funnyShow : Show String

Idris will default to the unnamed implementation when there is only one unnamed implementation in scope, regardless of the presence of named implementations. We can see that simply defining a named implementation of Show for String doesn't affect normal use of our greet function from earlier:

Hello "Tim"

We can, however, explicitly instruct Idris to use our named implementation, and get the expected result:

Hello Ha Ha, stole your string!

HLists

The Problem

From time to time, it becomes necessary to have values of multiple different types in a collection. In languages with less expressive type systems, this might require implementing a sum type/enum with a variant for each type we wish to contain, such as the following Rust example:

enum Heterogeneous {
    TString(String),
    Tu64(u64),
    ...
}

fn doThingsHeterogenously(xs: Vec<Heterogeneous>) -> ... {
    for x in xs {
       match x {
           TString(string) => ...,
           Tu64(number) => ...,
       } 
    }
}

This solution incurs a fair amount of boilerplate, and also has some other drawbacks. For instance, our Vec<Heterogeneous> type can't contain any values of any type that isn't explicitly addressed in the Heterogeneous enum, if we want our Vec to contain any other type, we have to go back and add it to the enum. If the Heterogeneous enum is exposed in the public api, then there are also semver concerns with adding new variants, and simply marking the enum #[non_exhaustive] may not be suitable in every case.

If we want to work with an open universe of types instead of a closed universe, to use the dependent typing parlance, Rust does provide another option: trait objects. We could instead write something like:

fn displayThingsHeterogenously(xs: Vec<Box<dyn Display>>) -> ... {
    for x in xs {
        let formatted = format!("{x}");
        ...
    }
}

This lets us, at least nominally, put any value of any type that implements Display in our Vec, but trait objects come with plenty of drawbacks of their own. Trait objects don't have a fixed size, so in general we can only talk about pointers to them, adding boilerplate. Additionally, not every trait is dyn-compatible(also known as object safe)⁵. Many of the more expressive features of the type system become off-limits for use in our trait if we want it to be dyn-compatible. For instance, methods in dyn-compatible traits aren't allowed to have any type parameters at all!

Idris has many more comprehensive solutions for us to employ, allowing us to get the best of both worlds, relative to the above Rust solutions, keeping our types fully concrete without forgetful upcasting, but still allowing us to keep our universes open and not arbitrarily restricted to a specifically enumerated list of types.

Definition

One of the simplest heterogeneous collection types in Idris is HList, a list like structure parameterized over a list of types where each type in the list describes the type contained in the corresponding position of the HList. HList can be defined like so:

namespace HListDefinition
  data HList' : List Type -> Type where
    Nil : HList' []
    (::) : (x : t) -> (xs : HList' ts) -> HList' (t :: ts)

In addition to collecting the types of the contained values into a list at the type level, this structure has a few other interesting properties:

• The length of an HList is also constrained by the list-of-types parameter to the type constructor
• The types of the contained values only ever appear in the definition of an HList as unbound lowercase implicits, which are erased. As such, the typing information for the HList need not exist at runtime, and their runtime representation is identical to that of a regular List or tuple⁶.

Usage

HLists are most useful when combined with other dependently typed constructs, serving as a foundational concept for type level programming, but they still have many uses on their own. As we have seen in Row Polymorphic Programming, they can be used to build ad-hoc struct-like entities with convenient syntax for the caller, to provide a simple example:

numberStringBool : HList [Nat, String, Bool] -> String
numberStringBool [number, string, bool] = "The number \{number} is \{string}: \{show bool}"

"The number 3 is even: False"

This simple usage isn't too much different from just using a tuple. Lets try to show off the type level programming capability a bit better by expressing a little bit of a non-trivial contract in the type. Say we want to be able to show a list of objects with separators between them, and we want those separators to be arbitrary strings that can be different in each position. For a list of n things, we can build a list of types to describe this collection by replicating the type n times and interspersing String into it:

showNThingsWithSeparators : Show t => 
  (n : Nat) -> (xs : HList (intersperse String (replicate n t))) -> String
showNThingsWithSeparators 0 [] = ""
showNThingsWithSeparators (S 0) [x] = show x
showNThingsWithSeparators (S (S k)) (x :: (y :: xs)) = 
  show x ++ y ++ showNThingsWithSeparators (S k) xs

We can then call this with a manually specified HList, and see that the compiler accepts it and it works as expected:

"123,456.000"

Now, if we get a bit lazy, and we want to call this function, but we don't actually want distinct separators in different positions, we can write a function to generate an appropriate HList from a List t and a constant separator:

intersperseH : Show t => 
  (xs : List t) -> (sep : String) -> HList (intersperse String (replicate (length xs) t))
intersperseH [] sep = []
intersperseH [x] sep = [x]
intersperseH (x :: (y :: xs)) sep = 
  x :: sep :: intersperseH (y :: xs) sep

And we can see it also works as expected:

"'a','b','c'"

The List of Types Isn't Special

Thinking back to our Rust example, where we had to lift the type arguments into ~special~ arguments, we can see that the List Type argument to the HList type constructor isn't ~special~ at all. Its just a normal list, that we can do normal list things to. And the types contained in that list behave just like regular values⁷ without the arbitrary restrictions that come with Rust's type arguments.

Think back to our id example above, where we showed that id is actually a function from a type to a monomorphic identity function. Consider this identity function over HLists:

hListId : HList ts -> HList ts
hListId [] = []
hListId (x :: xs) = x :: hListId xs

Applying our desugaring rules to its type signature, we get:

hListId' : {0 ts : List Type} -> HList ts -> HList ts

Instead of a function from a type to a monomorphic implementation, the structure of HList has given us a function from a list of types to a monomorphic implementation.

All

HList on its own is already pretty useful, but also somewhat limited. In the examples we've worked through so far, there are still all sorts of restrictions on the included types, such as the "either String or t" requirement in showNThingsWithSeperators. We haven't yet looked at anything equivalent to the Rust example of heterogeneous collections yet. To do that, we need a way to make general statements about all of the types in the list. This is where All comes in.

Definition

All "augments" a list with a witness that each value in the list satisfies a given "predicate". In this context, a predicate is a type of kind⁸ a -> Type, where a given value x : a satisfies a predicate Pred : a -> Type if a value of the type Pred x exists. Predicates are a quite general concept, interfaces can be thought of as predicates, and we will consider other examples as we continue through the article.

namespace AllDefinition
  data All : (p : a -> Type) -> (ts : List a) -> Type where
    Nil : All p []
    (::) : {0 x : a} -> (a : p x) -> (ps : AllDefinition.All p xs) 
      -> All p (x :: xs)

Notice how the types themselves still don't show up in the runtime representation, only the witnesses of the provided predicate. The types themselves need not exist at runtime, and in some situations, we can even get away with erasing the All entirely.

Notably, All can be considered a more fundamental concept than HList, since HList can be implemented in terms of All. The Idris standard library implements HList as simply an alias for All id⁹. As a predicate, id can be understood as a proof that an arbitrary type is inhabited, by way of presenting a value of that type, with no further restriction.

HLists Where Everything Implements an Interface

Think back to our examples of heterogeneous collections in Rust, with All in our toolkit, we can finally express the Idris equivalent:

displayH : All Show ts => HList ts -> String
displayH xs = 
  let shown : All (const String) _ = imapProperty Show show xs
      -- Our list has become homogenous, so we can forget that it was originally
      -- a heterogenous collection
      strings : List String = forget shown
  in "[\{joinBy ", " strings}]"

We can see that this works as expected:

[2.0, False, 11, "Hello!"]

Note that this does not have the drawback of the first Rust version, the "universe" of types it operates on is completely open, since Show can be implemented for any type anywhere. It also doesn't have the drawback of the second, there's no forgetful upcasting, or even casting at all! The types are still in their full, concrete forms, with no reference to them at runtime, we just don't have to reference the types directly as the All Show ts constraint ensures that each element in the HList is matched up with an appropriate Show implementation for its type.

To explore that concept more, lets manually implement the operation being performed by the imapProperty operation above:

showAll : All Show ts => HList ts -> List String
showAll {ts = []} @{[]} [] = []
showAll {ts = (t :: ts)} @{(show_x :: show_xs)} (x :: xs) = ?showAll_rhs

I've deliberately left it not fully implemented so we can inspect the hole and see what's going on with the types:

 0 t : Type
 0 ts : List Type
   show_x : Show t
   show_xs : All Show ts
   x : t
   xs : All id ts
------------------------------
showAll_rhs : List String

As you can see, the type of x, t, is erased¹⁰, as such it doesn't exist at runtime, and the evaluation of our function can't depend on what t is. Even though we are forbidden from inspecting the value of t, we don't have to, we can still tell that show_x constitutes a valid Show implementation for t, enabling us to call show x, just from the type signatures alone.

Let's complete the implementation and show that it works as expected:

showAll' : All Show ts => HList ts -> List String
showAll' @{[]} [] = []
showAll' @{_ :: _} (x :: xs) = 
  show x :: showAll' xs 

["1", "2.0", "True"]

Interface Implementations Aren't Special

In the Rust example, in order to achieve this type of "open universe" polymorphism, we had to upcast into a trait object, which is a ~special~ type of value that glues together a particular value and the trait implementation over it, but doesn't fully behave like the normal values of the system.

In contrast, interface implementations in Idris aren't ~special~, they are normal first class values with no special behavior. We also don't have to do this "gluing together" of the value and the associated implementation into a single value, by keeping the implementation and the associated value separate while keeping them paired through the type signatures, we are free to forget the type of the value at runtime, while still being able to statically enforce that a given implementation will only ever be invoked against a value with the correct type.

If we inspect the full type signature of showAll':

DependentNuggets.AnyAllLolnogenerics.showAll' : {0 ts : List Type} ->
All {a = Type} Show ts => HList ts -> List String

We can see that it is a function from a list of types to a function that accepts implementations of the Show interface for all of the types of the list, returning a monomorphic implementation of the underlying logic.

Closing the Universe

Predicates

Sometimes, the behavior of the first Rust implementation, restricting the set of allowed types in the collection, is desirable. Idris provides us a few different ways to do so. Since we've mentioned predicates before, we'll start with those.

As previously mentioned a predicate is a type of kind Pred : a -> Type, that is considered satisfied for a given value x : a when a value of the type Pred x exists. We have already looked at interfaces, which are a type of predicate over types, but we can also straightforwardly define a "closed" type predicate as a sum type:

data Allowed : Type -> Type where
  StringAllowed : Allowed String
  NatAllowed : Allowed Nat
  BoolAllowed : Allowed Bool

This particular predicate is satisfied for String, Nat, and Bool, with the individual constructors serving as proof that the respective type is allowed. We can see that proof search is able to find instances of Allowed for the allowed types:

BoolAllowed

We can also see that a compiler allows us to create a well formed HList of Allowed types:

acceptsAllowed : All Allowed ts => HList ts -> ()
acceptsAllowed _ = ()

thisAllowedIsValid : ()
thisAllowedIsValid = acceptsAllowed [the Bool True, the Nat 1, the String "Hello"]

And that it rejects attempts to include types that aren't allowed:

failing
  thisAllowedIsNotValid : ()
  thisAllowedIsNotValid = acceptsAllowed [the Double 1.0]

This approach gives us a few paths to implement our running example of displaying a heterogeneous list of things. As one approach, we can implement a conversion function from our Allowed witness to a Show implementation:

allowedToShow : Allowed t -> Show t
allowedToShow StringAllowed = %search
allowedToShow NatAllowed = %search
allowedToShow BoolAllowed = %search

We can then use this function to convert a value of All Allowed ts into a value of All Show ts and use our previously defined displayH function:

displayAllowed : All Allowed ts => HList ts -> String
displayAllowed @{allAllowed} xs = 
  let allShow : All Show ts = mapProperty allowedToShow allAllowed
  in displayH xs

[False, 42, "frog"]

If we wanted to, we could also directly pattern match on the witnesses ourselves, which gives us a little bit more flexibility at the cost of some verbosity. For example, we could choose to output strings verbatim, only using show for the other types:

displayAllowed' : All Allowed ts => HList ts -> String
displayAllowed' xs = 
  let strings : List String = allowedsToStrings xs
  in "[\{joinBy ", " strings}]"
  where
    allowedsToStrings : All Allowed ts' => HList ts' -> List String
    allowedsToStrings @{[]} [] = []
    allowedsToStrings @{(StringAllowed :: _)} (y :: ys) = 
      y :: allowedsToStrings ys
    allowedsToStrings @{(NatAllowed :: _)} (y :: ys) = 
      show y :: allowedsToStrings ys
    allowedsToStrings @{(BoolAllowed :: _)} (y :: ys) =
      show y :: allowedsToStrings ys

[False, 42, frog]

Explicit conversion

Instead of specifying our sum type as a predicate, we could, instead, build a normal enum-style sum type, and define a function from it to the corresponding type:

data Universe = TString | TNat | TBool

universeType : Universe -> Type
universeType TString = String
universeType TNat = Nat
universeType TBool = Bool

We'll also want a function to convert a list of Universe to a list of types, to avoid running into issues with the standard library's implementation of map:

universeTypes : List Universe -> List Type
universeTypes [] = []
universeTypes (x :: xs) = universeType x :: universeTypes xs

We can also implement a proof that every type in a list of types generated from a List Universe has a Show implementation:

universalShow : {us : List Universe} -> All Show (universeTypes us)
universalShow {us = []} = []
universalShow {us = (TString :: us)} = %search :: universalShow 
universalShow {us = (TNat :: us)} = %search :: universalShow
universalShow {us = (TBool :: us)} = %search :: universalShow

We can use our universeTypes function to define the list-of-types type argument to an HList in terms of a list of Universe values, and then invoke our universalShow proof to allow us to call displayH on that HList:

displayU : (us : List Universe) -> HList (universeTypes us) -> String
displayU us xs = displayH @{universalShow} xs

["cat", 5, False]

This approach can often be a little bit more verbose, but comes with advantages of its own. For instance, this approach enables relatively ergonomic building of types from runtime inputs, which will be covered in a future article.

Other Uses of All

All is also useful outside the context of HLists, as it can apply any predicate over any list. Just as an example, you can use All with the IsSucc¹¹ predicate, which is satisfied for Nats which are non-zero, to specify a list of non-zero numbers:

sumNonZeros : (xs : List Nat) -> All IsSucc xs => Nat
sumNonZeros xs = sum xs

We can see this function works when called on a list of non-zero numbers:

15

And we can also see that a call to sumNonZeros fails to compile if we try to include a 0 in the list:

failing
  oopsAZero : Nat
  oopsAZero = sumNonZeros [0, 1, 2, 3, 4, 5]

Any

Sometimes, making a blanket statement about all the types in a list is too strong of a statement. Lets dial it back a bit and just make a statement about one arbitrary element in a list, through the Any type.

Definition

A value of type Any p xs proves that at least one element of xs satisfies the predicate p by encoding the position of that element in the xs:

namespace AnyDefinition
  data Any' : (p : a -> Type) -> (xs : List a) -> Type where
    Here : {0 x : a} -> p x -> Any' p (x :: xs)
    There : Any' p xs -> Any' p (x :: xs)

Usage

Any is a bit more niche, so we'll be exploring a more contrived use-case for it. Imagine we are working with some row types, which must have at least one identifying column, but it doesn't matter where that identifying column is in the row. We want to display such row types with the identifier in front of the the row.

First, we must describe what types are allowed to be an identifier, to keep things simple, we'll define a predicate that only accepts Nat:

data Identifier : Type -> Type where
  INat : Identifier Nat

Now we can write our special display function and try it out:

displayWithIdent : Any Identifier ts => All Show ts => 
  HList ts -> String
displayWithIdent @{ident} xs = 
  let id = extractIdent ident xs
  in "\{id}: \{displayH xs}"
  where
    extractIdent : Any Identifier ts' -> HList ts' -> String
    extractIdent (Here INat) (z :: zs) = show z
    extractIdent (There x) (z :: zs) = extractIdent x zs

0: ["Cat", "meows", True, 0]

Concrete use cases for Any tend to be a bit more informed by the overall structure of the larger system, which makes it harder to give a brief survey with code examples, but other potential uses of any include:

• Requiring that at least one event handler in a list of handlers can deal with a specific type of event
• Requiring that a list of resource providing types contains at least one provider for a specific resource
• Requiring that at least one element in a regular, homogeneous list satisfies a given property

Other Less General Heterogeneous Collections

There are plenty of other heterogeneous collections to consider in Idris with all sorts of varied use cases.

Alternating

Data.List.Alternating provides a sort of restricted HList that alternates back and forth between two specific types, our showNThingsWithSeparators example from earlier can be thought of as using an ad-hoc implementation of Odd, the type of alternating list that starts and ends with the same type. Let's write an equivalent using Odd and try it out:

showAlternating : Show t => Odd t String -> String
showAlternating xs = 
  let strings = oddToStrings xs
  in joinBy "" strings
  where
    oddToStrings : Odd t String -> List String
    evenToStrings : Even String t -> List String
    oddToStrings (x :: xs) = show x :: evenToStrings xs
    evenToStrings [] = []
    evenToStrings (x :: xs) = x :: oddToStrings xs

1,234.56

Row Types

Row types are a form of augmented HList that provide all sorts of extra type-level programming tools.

DList and DMap

Dependent lists and dependent maps are both heterogeneous collections that derive typing information from some aspect of the contained data. We will be giving both of these structures the proper treatment they deserve in future articles.