A fascinating aspect of Lisp-based programming languages is that code is data and data is code. This property, called homoiconicity, is what makes Lisp macros so powerful. This sort of runtime operation done on arbitrary datatypes is called polytypism or datatype genericity. In Haskell, the following two packages provide datatype genericity:

While the former comes with `base`

, the latter is much easier to write generics code in, and this blog post introduces `generics-sop`

.

## Motivation

Generic programming is useful in avoiding writing of boilerplate implementations for each datatype that are otherwise similar in some way. This could be a (polytypic) function or a typeclass instance. For example, instead of having to manually write `FromJSON`

and `ToJSON`

instances for each of your datatypes, you can use generics to derive them automatically. Other examples include pretty printers, parsers, equality functions and route encoders.

## Basics

Before diving, we must understand the “SOP” in generics-**sop**.

### Datatypes are SOPs under the hood

Haskell has two kinds of datatypes:

- Algebraic data types, or ADTs
- Newtypes

Both ADTs and newtypes are a “sum-of-product” (SOP) under the hood. When writing generics-sop code, we operate on these SOPs rather than directly on the datatype, because every datatype is “polymorphic” in their SOP representation. The basic idea is that if you can write a function `SOP -> a`

, then you get `SomeDataType -> a`

for free for *any* `SomeDataType`

. This is called polytypism.

Consider the following ADT (from the `these`

package):

```
-- `These` is like `Either`, but with a 3rd possibility of representing both values.
data These a b
= This a
| That b
| These a b
```

Here, `These`

is a **sum** type, with `This`

, `That`

and `These`

being its three sum constructors. Each sum constructor themselves are **product** types - inasmuch as, say, the `a`

and `b`

in the 3rd constructor together represent a product type associated with *that* constructor. The type `These`

is therefore a “sum of product”.

### SOPs are tables

To gain better intuition, we may visualize the `These`

SOP in a table form:

Constructor | Arg 1 | Arg 2 | … |
---|---|---|---|

This | a | ||

That | b | ||

These | a | b |

As every Haskell datatype is a SOP, they can be (visually) reduced to a table like the above. Each row represents the sum constructor, and the individual cells to the right represent the arguments to the constructors (product type). We can drop the constructor *names* entirely and simplify the table as:

a | |

b | |

a | b |

(* These* type visually represented as a table)

Every cell in this table is a unique type. To define this table in Haskell we could use type-level lists, specifically a type-level *list of lists*. The outer list represents the sum constructor, and the inner list represents the products. The *kind* of this table type would then be `[[Type]]`

. Indeed this is what generics-sop uses. We can define the table type for `These`

in Haskell as follows:

```
type TheseTable a b =
'[ '[ a ]
'[ b ]
'[ a, b ] ]
```

If you are confused about this syntax, read the following “Interlude” section.

### Interlude: a foray into type-level programming

What is a “kind”? Kinds are to types what types are to terms. For example, the *type of* of the term `"Hello world"`

is `String`

. The latter is a “type,” whereas the former is a “term”. Furthermore we can go one level up and ask - what the *kind of* of the type `String`

is; and the answer is `Type`

. We can clarify this further by explicitly annotating the kinds of types when defining them (just as we annotate the types of terms when defining them):

```
-- Here, we define a term (2nd line) and declare its type (1st line)
someBool :: Bool
= True
someBool
-- Here, we define a type (2nd line) and declare its kind (1st line)
type Bool :: Type
data Bool = False | True
```

Parametrized types, such as `Maybe`

, have a type-level function as their kind:

```
type Maybe :: Type -> Type
data Maybe a = Nothing | Just a
```

Here we say that “the type `Maybe`

is of kind `Type -> Type`

”. In other words, `Maybe`

is a *type-level function* that takes a type of kind `Type`

as an argument and returns another type of the same kind `Type`

as its result.

Finally, we are now in a position to understand the kind of `TheseTable`

described in the prior section:

```
type TheseTable :: Type -> Type -> [[Type]]
type TheseTable a b =
'[ '[ a ]
'[ b ]
'[ a, b ] ]
```

`[Type]`

is the kind of type-level lists, and `[[Type]]`

is the kind of type-level lists of lists. The tick (`'`

) lifts a term into a type. So, while `True`

represents a *term* of type `Bool`

, `'True`

on the other hand represents a *type* of *kind* `Bool`

, just as `'[a]`

represents a type of the kind `[Type]`

. The tick “promotes” a term to be a type. See Datatype promotion in GHC user guide for details.

See An introduction to typeclass metaprogramming as well as Thinking with Types for more on type-level programming.

## Let’s play with SOPs

Enough theory, let’s get our hands dirty in GHCi. If you use Nix, you can clone this repo and run `bin/repl`

to get GHCi with everything configured ahead for you.

```
$ git clone https://github.com/srid/generics-sop-examples.git
$ cd ./generics-sop-examples
$ bin/repl
[1 of 1] Compiling Main ( src/Main.hs, interpreted )
Ok, one module loaded.
*Main>
```

The project already has `generics-sop`

and `sop-core`

added to the .cabal file, so you should be able to import it:

`> import Generics.SOP`

We also have the `these`

package added to the .cabal file because it provides the above `These`

type from `Data.These`

module. To explore the SOP representation of the `These`

type, let us do some bootstrapping:

```
> import Data.These
> instance Generic (These a b) -- Derive generics-sop instance
> let breakfast = These "Egg" "Sausage" :: These String String
```

We derived `Generic`

on the type and created a term value called `breakfast`

(we are eating both eggs and sausages). To get the SOP representation of this value, we can use `from`

:

```
> unSOP . from $ breakfast
S (S (Z (I "Egg" :* I "Sausage" :* Nil)))
```

Well explain the above value structure in a bit, but the key thing to realize is that this value corresponds to the 3rd row in the SOP table for `These`

:

String | |

String | |

String | String |

Because `breakfast`

is a value of the 3rd constructor of `These`

and it contains two values (the product of “Egg” and “Sausage”). The corresponding Haskell type for this table:

```
type TheseTable :: [[Type]]
type TheseTable =
String ]
'[ '[ String ]
'[ String, String ]
'[ ]
```

This type is automatically provided by `generics-sop`

whenever we derive a `Generic`

instance for the type in question. We did precisely that further above by evaluating `instance Generic (These a b)`

in GHCi. Instead of manually defining `TheseTable`

as above, deriving `Generic`

gives it for free, in the form of `Code a`

(viz. `Code (These a b)`

).

```
> :k Code (These String String)
Code (These String String) :: [[Type]]
```

In brief, remember this: `Code a`

gives us the SOP table *type* for the datatype `a`

. Now how do we get the SOP table *value*? That is what `from`

is for:

```
> :t (unSOP . from $ breakfast)
. from $ breakfast)
(unSOP :: NS
@[Type]
NP @Type I)
(:)
(('@[Type]
:) @Type [Char] ('[] @Type))
((':)
(('@[Type]
:) @Type [Char] ('[] @Type))
((':)
(('@[Type]
:) @Type [Char] ((':) @Type [Char] ('[] @Type)))
(('@[Type])))) ('[]
```

That is quite a mouthful because type-level lists are not represented cleanly in GHCi. But we can reduce it (in our mind) to the following

```
> :t (unSOP . from $ breakfast)
. from $ breakfast)
(unSOP :: NS (NP I) '[ [String], [String], [String, String] ]
```

Notice how this is more or less isomorphic to our `TheseTable`

definition above. We will explain the `NS`

and `NP`

parts next.

### Interlude: `NS`

& `NP`

You wonder what the `NS (NP I)`

part refers to in our table type above. `NS`

is a n-ary sum; and `NP`

an n-ary product. These are explained well in section 2 of Applying Type-Level and Generic Programming in Haskell, but for our purposes - you can treat `NS`

as similar to the `Nat`

type from the fin package, and `NP`

as being similar to the `Vec`

type from the vec package.

The difference is that unlike `Vec`

(a homogenous list), `NP`

is a heterogenous list whose element types are specified by a type-level list.

```
> :k NP I '[String, Int]
NP I '[String, Int] :: Type
```

Just like `Vec`

can enforce the size of its homogenous list, `NP`

is a heterogenous list of exactly size 2. However, unlike `Vec`

we also say that the first element is of type `String`

and the second (and the last) element is of type `Int`

(hence a heterogenous list). To create a value of this heterogeneous list:

```
> I "Meaning" :* I 42 :* Nil :: NP I '[String, Int]
I "Meaning" :* I 42 :* Nil
```

This syntax should be unsurprising because `Nil`

and `(:*)`

are the constructors of the `NP`

type:

```
> :info NP
data NP :: (k -> Type) -> [k] -> Type where
Nil :: NP f '[]
(:*) :: f x -> NP f xs -> NP f (x ': xs)
```

The `I`

is the identity functor, but it could also be something else like `Maybe`

:

```
> Nothing :* Just 42 :* Nil :: NP Maybe '[String, Int]
Nothing :* Just 42 :* Nil
```

`NS`

is the same, except now we are representing the same characteristics (heterogeneity) but for the sum type instead of a product type. A sum of length ‘n’ over some functor ‘f’:

```
> :info NS
data NS :: (k -> Type) -> [k] -> Type where
Z :: f x -> NS f (x ': xs)
S :: NS f xs -> NS f (x ': xs)
```

When the value is `Z`

it indicates the first sum constructor; when it is `S . Z`

it is the second, and so on. Our `breakfast`

value above uses `These`

, which is the 3rd constructor. So, to construct the SOP representation of this value directly, we would use `S . S . Z`

. This is exactly what we saw above (repeated here):

```
-- Note the `S . S . Z`
> unSOP . from $ breakfast
S (S (Z (I "Egg" :* I "Sausage" :* Nil)))
>
> :t (unSOP . from $ breakfast)
. from $ breakfast)
(unSOP :: NS (NP I) '[ [String], [String], [String, String] ]
```

`NS`

’s functor is a `NP I`

, and so the inner value of that sum choice is an n-ary product (remember: we are working with a sum-of-product), whose value is `I "Egg" :* I "Sausage" :* Nil`

. Putting that product inside a sum, we get `S (S (Z (I "Egg" :* I "Sausage" :* Nil)))`

.

### Code as data; data as code

Ther SOP representation of `These`

can be manually constructed. First we build the constructor arguments (product), and then we build the constructor itself (sum):

```
> let prod = I "Egg" :* I "Sausage" :* Nil :: NP I '[String, String]
> let sum = S $ S $ Z prod :: NP I '[[String], [String], [String, String]]
> :t sum
sum :: NS (NP I) '[[String], [String], [String, String]]
```

And from this representation, we can produce a value of type `These`

easily, using `to`

:

```
> to @(These String String) (SOP sum)
These "Egg" "Sausage"
```

Let us stop for a moment and reflect on what we just did. By treating the type-definition of `These`

(“code”) as a generic `SOP`

table (“data”) – i.e., code as data – we are able to generate a value (“code”) for that type (“data”) – ie., data as code – but without using the constructors of that type. This is generic programming in Haskell; you program *generically*, without being privy to the actual type used.

This concludes the section on playing with SOPs. Now let us do something useful.

## Example 1: generic equality

GHC’s stock deriving can be used to derive instances for builtin type classes, like `Eq`

, on user-defined datatypes. This works for builtin type classes, but generics-sop (as well as GHC.Generics) comes in handy when you want to derive generically for arbitrary typeclasses. For a moment, let us assume that GHC had no support for stock deriving; how will we derive our `Eq`

instance?

We want a function `geq`

that takes *any* datatype `a`

(this makes the function polytypic), and does equality check on its arguments. In effect, we want:

`geq :: Generic a => a -> a -> Bool`

This function can be further broken down to operate on SOP structures directly, so as to “forget” the specific `a`

:

```
geq :: forall a. Generic a => a -> a -> Bool
= geq' @a (unSOP $ from x) (unSOP $ from y)
geq x y
geq' :: NS (NP I) (Code a) -> NS (NP I) (Code a) -> Bool
= undefined geq'
```

Our problem has now been reduced to operating on SOP tables, and our task is to implement `geq'`

.

At this point you are probably thinking we can just case-match on the arguments, but remember that the n-ary sum type `NS`

is a GADT (its type index is dependent on the sum constructor). We have to instead case-match at the *type-level* as it were. This is what type-classes are for. The general pattern is that when wanting a `foo`

that case-match’es at type-level, we write a type-class `Foo`

and write instances for each case-match pattern.

### Naive implementation

For pedagogic reasons, we begin with a naive implementation of `geq'`

to illustrate the above. We need a `sumEq`

function that checks equality of first constructor and then recurses for others; it will case-match on the outer list. Likewise, for each sum constructor, we will need a `prodEq`

that checks equality of its products; and it does so, similarly, by checking equality of the first product and then recurses for the rest; it will case-match on the inner list.

```
geq' :: SumEq (Code a) => NS (NP I) (Code a) -> NS (NP I) (Code a) -> Bool
= sumEq
geq'
-- `xss` is a type-level list of lists; `Code a`
class SumEq xss where
sumEq :: NS (NP I) xss -> NS (NP I) xss -> Bool
instance SumEq '[] where
= \case
sumEq
instance (ProdEq xs, SumEq xss) => SumEq (xs ': xss) where
-- Both values are the same constructor; so check equality on their products,
-- using `prodEq`.
Z x) (Z y) = prodEq x y
sumEq (-- Recurse on next sum constructor.
S x) (S y) = sumEq x y
sumEq (-- Mismatching sum constructor; equality check failed.
= False
sumEq _ _
class ProdEq xs where
prodEq :: NP I xs -> NP I xs -> Bool
instance ProdEq '[] where
Nil Nil = True
prodEq
instance (Eq x, ProdEq xs) => ProdEq (x ': xs) where
-- First product argument should be equal; then we recurse for rest of arguments.
:* xs) (y :* ys) = x == y && prodEq xs ys prodEq (x
```

Notice how in the first instance for `SumEq`

we are “pattern matching” as it were at the type-level and defining the implementation for the scenario of zero sum constructors (not inhabitable). Then, inductively, we define the next instance using recursion. When both arguments are at `Z`

, we match their products, using `prodEq`

which is defined similarly. Otherwise, we recurse into the successor constructor (the `x`

in `S x`

). The story for `ProdEq`

is similar.

Finally, we can test that it works:

```
> geq (This True) (That False)
False
> geq (These 42 "Hello") (These 42 "Hello" :: These Int String)
True
```

We just implemented an equality function that works for *any* datatype (with `Generic`

instance).

### Combinator-based implementation

Hopefully, the above naive implementation is illustratory of how one can “transform” SOP structures straightforwardly using typeclasses. N-ary sums and products need to be processed at type-level, so it is not uncommon to write new type-classes to dispatch on their constructors, as shown above. Typically, however, you do not have to do that because `generics-sop`

provides combinators for common operations. Here, we will rewrite the above implementation using these combinators.

The combinators are explained in depth in ATLGP. We will introduce a few in this post. The particular combinators we need for `geq`

are:

Combinator | Description | Typeclass it replaces |
---|---|---|

`hcliftA2` | Lift elements of a NP or NS using given function | `ProdEq` |

`hcollapse` | Convert heterogenous structure into homogenous value | `ProdEq` |

`ccompare_NS` | Compare two `NS` values | `SumEq` |

To appreciate the value of these particular combinators, notice the 3rd column indicating the type-class it intends to replace. Withtout further ado, here is the new (compact) implementation:

```
geq :: forall a. (Generic a, All2 Eq (Code a)) => a -> a -> Bool
= geq' @a (from x) (from y)
geq x y
geq' :: All2 Eq (Code a) => SOP I (Code a) -> SOP I (Code a) -> Bool
SOP c1) (SOP c2) =
geq' (Proxy @(All Eq)) False eqProd False c1 c2
ccompare_NS (where
eqProd :: All Eq xs => NP I xs -> NP I xs -> Bool
=
eqProd p1 p2 &&) True $
foldl' ($ hcliftA2 (Proxy :: Proxy Eq) eqTerm p1 p2
hcollapse where
eqTerm :: forall a. Eq a => I a -> I a -> K Bool a
=
eqTerm a b K $ a == b
```

This code introduces two more aspects to `generics-sop`

:

**Constraint propagation**: When generically transforming SOP structures we want to be able to “propagate” inner constraints outwardly, and this is what the`Proxy`

class is being used for here.`All c xs`

simply is an alias for`(c x1, c x2, ...)`

where`xs`

is a type-level list; likewise,`All2 c xss`

is`c x11, c x12, ...`

where`xss`

is type-level list of lists (ie.,`Code a ~ xss`

). Clearly, we want the`Eq`

constraint in table elements to apply to the whole table row and thereon to the table itself. And`All2 Eq (Code a)`

on`geq'`

specifies this.**Constant functor**: The constant functor`K`

is defined as`data K a b = K a`

; it “discards” the second type parameter, always containing the first. Where you see`K Bool a`

we are discarding the polymorphic`a`

(the type of the cell in the table), and returning the (constant) type`Bool`

. When we transform the structure to be over`K`

(using`hcliftA2`

), we are essentially making the structure*homogenous*in its elements, which in turn allows us to “collapse” it using`hcollapse`

to get a single value out of it (which is what we need to be the result of`geq`

).

This is just a brief taste of generics-sop combinators. Read ATLGP for details, and we shall introduce more in the examples below.

#### Interlude: Specialized combinators

Most combinators are polymorphic over the containing structure, and as such their type signatures can be pretty complex to understand. For this reason, you might want to begin with using their *monomorphized* versions which have simpler type signatures. For example, the polymorphic combinator `hcollapse`

has the following signature that makes it possible to work with any structure (`NS`

or a `NP`

, etc).

`hcollapse :: SListIN h xs => h (K a) xs -> CollapseTo h a`

This signature is not particularly easier to understand if you are not very familiar with the library. But the monomorphized versions, such as that for `NS`

, are more straightforward to understand:

`collapse_NP :: NP (K a) xs -> [a]`

These specialized versions typically are suffixed as above (i.e., `_NP`

).

## Example 2: route encoding

In the first example above we demonstrated how to use generics-sop to generically implement `eq`

. Here, we will show a more interesting example. Specifically, how to represent routes for a statically generated site using algebraic data types. We will derive encoders (`route -> FilePath`

) for them automatically using generics-sop.

Imagine you are writing a static site in Haskell^{1} for your blog posts. Each “route” in that site corresponds to a generated `.html`

file. We will use ADTs to represent the routes:

```
data Route
= Route_Index -- index.html
| Route_Blog BlogRoute -- blog/*
data BlogRoute
= BlogRoute_Index -- blog/index.html
| BlogRoute_Post PostSlug -- blog/${slug}.html
newtype PostSlug = PostSlug {unPostSlug :: Text}
```

To compute the path to the `.html`

file for each route, we need a function `encodeRoute :: r -> FilePath`

. It is worth creating a typeclass for it because we can recursively encode the ADT:

```
-- Class of routes that can be encoded to a filename.
class IsRoute r where
encodeRoute :: r -> FilePath
```

### Manual implementation

Before writing generic implementation, it is always useful to write the implementation “by hand”. Doing so enables us to begin to build an intuition for what the generic version will look like.

```
-- This instance will remain manual.
instance IsRoute PostSlug where
PostSlug slug) = T.unpack slug <> ".html"
encodeRoute (
-- These instances eventually will be generalized.
instance IsRoute BlogRoute where
= \case
encodeRoute BlogRoute_Index -> "index.html"
BlogRoute_Post slug -> "post" </> encodeRoute slug
instance IsRoute Route where
= \case
encodeRoute Route_Index -> "index.html"
Route_Blog br -> "blog" </> encodeRoute br
```

There is nothing we can do about `PostSlug`

instance because it is not an ADT, but we *do* want to generically implement `encodeRoute`

for both `BlogRoute`

and `Route`

generically.

### Identify the general pattern

After writing the implementation manually, the next step is to make it as general as possible. Try to extract the “general pattern” behind these manual implementations. Looking at the instances above, we can conclude the general pattern as follows:

- To encode
`Foo_Bar`

in a datatype`Foo`

, we drop the`Foo_`

, and take the`Bar`

. Then we convert it to`bar.html`

. - If a sum constructor has arguments, we check that it has exactly one argument (arity <=1). Then call
`encodeRoute`

on that argument, and append it to the constructor’s encoding using`/`

.- For example, to encode
`BlogPost_Post (PostSlug "hello")`

we first encode the constructor as`"post"`

, then encode the only argument as`encodeRoute (PostSlug "hello")`

which reduces to`"hello.html"`

, thus producing the encoding`"post/hello.html"`

. Finally when encoding`Route_Blog br`

- this gets encoded ito`"blog/post/hello.html"`

, inductively.

- For example, to encode

### Write the generic version

Having identified the general pattern, we are now able to write the generic version of `encodeRoute`

. Keep in mind the above pattern while you follow the code below.

```
gEncodeRoute :: Generic r => r -> FilePath
= undefined gEncodeRoute
```

To derive route encoding from the constructor name, we need the datatype metadata (provided by `HasDatatypeInfo`

) from generics-sop. `constructorInfo . datatypeInfo`

gives us the constructor information, from which we will determine the final route encoding using the `hindex`

combinator. Effectively, this enables us to produce `"foo.html"`

from a sum constructor like `Route_Foo`

.

```
gEncodeRoute :: forall r.
Generic r, All2 IsRoute (Code r), All IsRouteProd (Code r), HasDatatypeInfo r) =>
(-> FilePath
r = gEncodeRoute' @r (from x)
gEncodeRoute x
gEncodeRoute' :: forall r.
All2 IsRoute (Code r), All IsRouteProd (Code r), HasDatatypeInfo r) =>
(SOP I (Code r) -> FilePath
SOP x) =
gEncodeRoute' (-- Determine the contructor name and then strip its prefix.
let ctorNames :: [ConstructorName] =
$ hmap (K . constructorName) $ datatypeCtors @r
hcollapse = ctorNames !! hindex x
ctorName = ctorStripPrefix @r ctorName
ctorSuffix -- Encode the product argument, if any, otherwise end the route string with ".html"
in case hcollapse $ hcmap (Proxy @IsRouteProd) encProd x of
Nothing -> ctorSuffix <> ".html"
Just p -> ctorSuffix </> p
where
encProd :: (IsRouteProd xs) => NP I xs -> K (Maybe FilePath) xs
=
encProd K . hcollapseMaybe . hcmap (Proxy @IsRoute) encTerm
encTerm :: IsRoute b => I b -> K FilePath b
=
encTerm K . encodeRoute . unI
datatypeCtors :: forall a. HasDatatypeInfo a => NP ConstructorInfo (Code a)
= constructorInfo $ datatypeInfo (Proxy @a)
datatypeCtors
ctorStripPrefix :: forall a. HasDatatypeInfo a => ConstructorName -> String
=
ctorStripPrefix ctorName let name = datatypeName $ datatypeInfo (Proxy @a)
in maybe (error "ctor: bad naming") (T.unpack . T.toLower) $
$ name <> "_") (T.pack ctorName) T.stripPrefix (T.pack
```

`hcollapse`

should be familiar; and `hcmap`

is just an alias of `hcliftA`

(analogous to `hcliftA2`

used in the above example). New here is `hcollapseMaybe`

which is a custom version of `hcollapse`

we defined to constrain the number of products to be either zero or one (as it would not make sense for a route tye otherwise); its full implementation^{2} is available in the source.

Finally, we make use of `DefaultSignatures`

to provide a default implementation in the `IsRoute`

class:

```
class IsRoute r where
encodeRoute :: r -> FilePath
encodeRoute ::
defaultGeneric r, All2 IsRoute (Code r), HasDatatypeInfo r) =>
(->
r FilePath
= gEncodeRoute encodeRoute
```

This, in turn, allows us to derive `IsRoute`

arbitrarily via `DeriveAnyClass`

, which is to say that we get our `IsRoute`

instances for “free”:

```
data Route
= Route_Foo
| Route_Blog BlogRoute
deriving stock (GHC.Generic, Eq, Show)
deriving anyclass (Generic, HasDatatypeInfo, IsRoute)`
```

`encodeRoute Route_Foo`

now returns `"foo.html"`

and `encodeRoute $ Route_Blog BlogRoute_Index`

returns `"blog/index.html"`

, all without needing boilerplate implementation.

## Example 3: route decoding

As a final example, we shall demonstrate what it takes to *construct* new values. Naturally, our `IsRoute`

class above needs a new method, `decodeRoute`

for the reverse conversion (perhaps you want to check the validity of links in the generated HTML):

```
class IsRoute r where
-- | Encode a route to file path on disk.
encodeRoute :: r -> FilePath
-- | Decode a route from its encoded filepath
decodeRoute :: FilePath -> Maybe r
gDecodeRoute :: forall r.
Generic r, All2 IsRoute (Code r), HasDatatypeInfo r) =>
(FilePath -> Maybe r
= undefined gDecodeRoute fp
```

`SList`

Generically constructing values is a little more involved, where it useful to know about singleton for type-level lists, `SList`

.

```
data SList :: [k] -> Type where
SNil :: SList '[]
SCons :: SListI xs => SList (x ': xs)
-- | Get hold of an explicit singleton (that one can then
-- pattern match on) for a type-level list
--
sList :: SListI xs => SList xs
= ... sList
```

We require heavy use of `sList`

to generically implement `decodeRoute`

. `sList`

pretty much allows us to “case-match” on the type-level list and build our combinators accordingly, as we will see below.

### Anamomrphism combinators

To implement `decodeRoute`

generically, we are looking to construct a `NS (NP I) (Code r)`

depending on which constructor the first path segment of `fp`

matches with. Then, we recurse into constructing the inner route for the sum constructor’s (only and optional) product type. This recursive building of values is called anamorphism. In particular, we need two anamorphisms: one for the outer sum and another for the inner product.

`generics-sop`

already provides `cana_NS`

and `cana_NP`

as anamorphisms for `NS`

and `NP`

respectively. However we need a slightly different version of them, to return `Maybe`

values instead. We shall define them (prefixed with `m`

) accordingly as follows (note the use of `sList`

):

```
-- | Like `cana_NS` but returns a Maybe
mcana_NS ::
forall c proxy s f xs.
All c xs) =>
(->
proxy c forall y ys. c y => s (y ': ys) -> Either (Maybe (f y)) (s ys)) ->
(->
s xs Maybe (NS f xs)
= go sList
mcana_NS _ decide where
go :: forall ys. (All c ys) => SList ys -> s ys -> Maybe (NS f ys)
SNil _ = Nothing
go SCons s = case decide s of
go Left x -> Z <$> x
Right s' -> S <$> go sList s'
-- | Like `cana_NP` but returns a Maybe
mcana_NP ::
forall c proxy s f xs.
All c xs) =>
(->
proxy c forall y ys. (c y, SListI ys) => s (y ': ys) -> Maybe (f y, s ys)) ->
(->
s xs Maybe (NP f xs)
= go sList
mcana_NP _ uncons where
go :: forall ys. (All c ys) => SList ys -> s ys -> Maybe (NP f ys)
SNil _ = pure Nil
go SCons s = do
go <- uncons s
(x, s') <- go sList s'
xs pure $ x :* xs
```

### Implement `gDecodeRoute`

Now we are ready to use a combination of `sList`

, `mcana_NS`

and `mcana_NP`

to implement `gDecodeRoute`

:

```
gDecodeRoute :: forall r.
Generic r, All IsRouteProd (Code r), All2 IsRoute (Code r), HasDatatypeInfo r) =>
(FilePath -> Maybe r
= do
gDecodeRoute fp -- We operate on first element of the filepath, and inductively decode the rest.
: restPath <- pure $ splitDirectories fp
basePath -- Build the sum using an anamorphism
. SOP
to <$> mcana_NS @IsRouteProd @_ @_ @(NP I)
Proxy
(anamorphismSum basePath restPath)@r)
(datatypeCtors where
-- The `base` part of the path should correspond to the constructor name.
anamorphismSum :: forall xs xss.
IsRouteProd xs =>
FilePath ->
FilePath] ->
[NP ConstructorInfo (xs ': xss) ->
Either (Maybe (NP I xs)) (NP ConstructorInfo xss)
:* ps) =
anamorphismSum base rest (p Right ps) $ do
fromMaybe (let ctorSuffix = ctorStripPrefix @r (constructorName p)
Left <$> case sList @xs of
SNil -> do
-- For constructors without arguments, we simply expect the `rest`
-- of the path to be empty.
$ ctorSuffix <> ".html" == base && null rest
guard pure $ Just Nil
SCons -> do
-- For constructors with an argument, we ensure that the constructor
-- name matches the base part and then recurse into decoding the
-- argument itself.
$ ctorSuffix == base
guard pure $
@_ @_ @_ @I
mcana_NP Proxy @IsRoute)
(
anamorphismProductProxy
where
anamorphismProduct :: forall y1 ys1.
IsRoute y1, SListI ys1) =>
(Proxy (y1 ': ys1) -> Maybe (I y1, Proxy ys1)
Proxy = case sList @ys1 of
anamorphismProduct -- We "case match" on the rest of the products, to handle the scenario
-- of there being exactly one product.
SNil -> do
-- Recurse into the only product argument
$ not $ null rest
guard <- decodeRoute @y1 $ joinPath rest
r' pure (I r', Proxy)
SCons ->
-- Not reachable, due to HCollapseMaybe constraint
Nothing
```

We split the path `fp`

and process the first path segment by matching it with one of the sum constructors. In `anamorphismSum`

we handle the two cases of null product constructor and singleton product constructor (`mcana_NS`

is responsible for recursing into other sum constructors). For null product, we match the file path with “${constructorSuffix}.html” and return immediately. For a single product case, we use `mcana_NP`

to build the product. `anammorphismProduct`

uses `sList`

to case match on the rest of the products (i.e. 2nd, etc.) - and calls `decodeRoute`

on the first product only if the rest is empty, which in turn requires us to the `IsRoute`

constraint all the way above.

Finally, we use `DefaultSignatures`

to specify a default implementation in `IsRoute`

class.

### Putting it all together

We can test that our code works in ghci:

```
> import RouteEncoding
> encodeRoute Route_Index
"index.html"
> decodeRoute @Route $ encodeRoute Route_Index
Just Route_Index
```

To be completely sure, we can test it with inductive route values:

```
> encodeRoute $ Route_Blog $ BlogRoute_Post "hello"
"blog/post/hello.html"
> decodeRoute @Route "blog/post/hello.html"
Just (Route_Blog (BlogRoute_Post "hello"))
>
```

This concludes our introduction to `generics-sop`

.

## Further information

- Source code for this blog post
- This ZuriHac talk provides a good introduction to generics-sop
- Applying Type-Level and Generic Programming in Haskell by Andres Löh acts as a lengthy tutorial cum documentation for generics-sop

In particular, we create a

`HCollapseMaybe`

constraint that limits`hcollapse`

to work on at most 1 product:`class HCollapseMaybe h xs where hcollapseMaybe :: SListIN h xs => h (K a) xs -> Maybe a instance HCollapseMaybe NP '[] where = Nothing hcollapseMaybe _ instance HCollapseMaybe NP '[p] where K x :* Nil) = Just x hcollapseMaybe ( instance (ps ~ TypeError ('Text "Expected at most 1 product")) => HCollapseMaybe NP (p ': p1 ': ps) where = Nothing -- Unreachable hcollapseMaybe _ class (All IsRoute xs, HCollapseMaybe NP xs) => IsRouteProd xs instance (All IsRoute xs, HCollapseMaybe NP xs) => IsRouteProd xs`

Then we change

`encProd`

to be:`encProd :: (IsRouteProd xs) => NP I xs -> K (Maybe FilePath) xs = encProd K . hcollapseMaybe . hcmap (Proxy @IsRoute) encTerm`

While propagating the

`All IsRouteProd (Code r)`

constraint all the way up.↩︎