`Universe` - but for small and finite enumeration of ADTs

Question

I want to generically derive something like Universe for user's route type defined in terms of ADTs.

Problem: I can use neither Enum/Bounded nor Universe - because they are not safe. The default instances on types like Int64 can lead to gazillion routes being generated.

The following route is valid, and should be accepted because there is a small and finite number of routes:

data R = Index | Blog BlogR
data BlogR = Foo | Bar

The following route is invalid, and should not be accepted because there is an infinite number of routes generateble due to String. Neither should finitely enumerable types like Int64 be accepted.

data R = Index | Blog BlogR
data BlogR = Post String

The following route seems valid, but it should not be accepted either due to recursion.

data R = Index | Blog BlogR
data BlogR = Foo | Bar | Rec R

Questions:

Is there an existing type class that captures this constraint? If not, I would create one.
How to generically (generics-sop?) derive instances to capture this constraint, and fail with an user-friendly TypeError on invalid types?
Are there better ways of approaching this problem? Ultimately, I want a default implementation for IsRoute r => allRoutes :: [r]. At the moment, I use Enum and Bounded (see real-world code here) which is limiting because it cannot handle the first route type above.

user_7203016 · Answer

No, there's no existing type class that captures this type of constraint.

The challenge in defining a generics-based answer seems to be ruling out the recursion, as demonstrated below. I think the simplest approach is probably to use a counter that sets an upper limit on the "depth" of a type. The alternative would be to keep a type-level list of types already visited which seems like way too much trouble to be worth it.

So, here's a solution that uses GHC.Generics together with a type family constraint to enforce non-recursion (or technically, limited "depth" of the type).

Perhaps you're already familiar with the general GHC.Generics approach, but for completeness, here's how we'd put together a solution without worrying about recursion yet. We start with the type class we want to define:

class Small a where
  universe :: [a]

Then, we introduce a stylized generic type class, where the generic type a is replaced by a type f p such that f will play the role of the type-level representation Rep a of the type a we want to handle generically, while p is a dummy type variable that's never used:

import GHC.Generics

class GSmall f where
  guniverse :: [f p]

Instances of the GSmall type class are defined on types from GHC.Generics that represent meta information, sum and product types, and constructor fields.

For meta information (e.g., names of fields, etc.), generic classes like GSmall that want to ignore it should simply "get the types right" by wrapping or unwrapping with the M1 constructor, as appropriate. Here, we add M1 to every element of the universe list:

instance GSmall f => GSmall (M1 i c f) where
  guniverse = map M1 guniverse

For sum and product types, we need instances for the null sum (Void) and the null product (()) represented by generic types V1 and U1 respectively:

-- handle uninhabited type Void
instance GSmall V1 where
  guniverse = []
-- handle unit
instance GSmall U1 where
  guniverse = [U1]

For binary sums, the type level representation uses the operator :+: while the generic inhabitants are represented by the L1 and R1 constructors respectively. Here, by wrapping with the right constructors, we call guniverse polymorphically on the left and right types of the sum:

{-# LANGUAGE TypeOperators #-}

instance (GSmall f, GSmall g) => GSmall (f :+: g) where
  guniverse = map L1 guniverse ++ map R1 guniverse

For binary products, the process is similar, except we want to generate all combinations of the left and right side of the product:

instance (GSmall f, GSmall g) => GSmall (f :*: g) where
  guniverse = [f :*: g | f <- guniverse, g <- guniverse]

Finally, we handle constructor fields of type a by looping back to the concrete Small class:

instance Small a => GSmall (K1 r a) where
  guniverse = map K1 universe

If desired, we can add a default definition for universe in the Small class:

{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}

class Small a where
  universe :: [a]
  default universe :: (Generic a, GSmall (Rep a)) => [a]
  universe = universeGeneric

universeGeneric :: (Generic a, GSmall (Rep a)) => [a]
universeGeneric = map to guniverse

To use this generic instance, we write

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeApplications #-}

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = Foo | Bar deriving (Show, Generic)

instance Small Route
instance Small BlogR

main = print $ universe @Route

If you want to use a non-generic instance for some types, you can do that as well by overriding the default universe instance:

universeEnum :: (Bounded a, Enum a) => [a]
universeEnum = [minBound..maxBound]

data BlogR = Foo | Bar deriving (Show, Enum, Bounded)

instance Small BlogR where universe = universeEnum

Here's the complete solution so far:

{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

import GHC.Generics

class Small a where
  universe :: [a]
  default universe :: (Generic a, GSmall (Rep a)) => [a]
  universe = universeGeneric

class GSmall f where
  guniverse :: [f p]

universeGeneric :: (Generic a, GSmall (Rep a)) => [a]
universeGeneric = map to guniverse

universeEnum :: (Bounded a, Enum a) => [a]
universeEnum = [minBound..maxBound]

instance GSmall f => GSmall (M1 i c f) where
  guniverse = map M1 guniverse
instance GSmall V1 where
  guniverse = []
instance GSmall U1 where
  guniverse = [U1]
instance (GSmall f, GSmall g) => GSmall (f :+: g) where
  guniverse = map L1 guniverse ++ map R1 guniverse
instance (GSmall f, GSmall g) => GSmall (f :*: g) where
  guniverse = [f :*: g | f <- guniverse, g <- guniverse]
instance Small a => GSmall (K1 r a) where
  guniverse = map K1 universe

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = Foo | Bar deriving (Show, Generic)

instance Small Route
-- use generic
instance Small BlogR
-- or enum-based
-- instance Small BlogR where universe = universeEnum

main = print $ universe @Route

If you try to generate an instance for a non-recursive, non-small type (using Int, for example):

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = PostId Int deriving (Show, Generic)

instance Small Route
instance Small BlogR  -- error

you get an error:

No instance for (Small Int)

which seems user-friendly enough without a TypeError.

The one problem is that recursive types are accepted, including lists, so we can define:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = PostId String deriving (Show, Generic)

instance Small Route
instance Small BlogR
instance Small String
instance Small Char where universe = universeEnum

and get valid instances. Same for your explicitly recursive example.

I think the simplest way to address this is to define a separate generic type family constraint to check that a type is non-recursive (or more exactly, has a limited depth). This should include a generics based closed type family, something like the following. Note that the top parameter is used here to remember the top-level type for error messages. The generic type being processed is f, and the family yields an empty constraint if the depth of f doesn't exceed the depth "countdown" in n, and a TypeError otherwise:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import GHC.TypeLits

type family GClosed n top f :: Constraint where
  GClosed 0 top f = TypeError (Text "Depth limit exceeded by type: " :<>: ShowType top)
  GClosed n top (M1 i c f) = GClosed n top f
  GClosed n top V1 = ()
  GClosed n top U1 = ()
  GClosed n top (f :+: g) = (GClosed n top f, GClosed n top g)
  GClosed n top (f :*: g) = (GClosed n top f, GClosed n top g)
  GClosed n top (K1 r a) = NClosed (n-1) top a

Note that the final case for K1 calls into an associated NClosed type family in the Small class, defaulting to the generic assessment of being "closed" via GClosed:

class Small a where
  ...
  type NClosed (n :: Nat) top a :: Constraint
  type instance NClosed n top a = GClosed n top (Rep a)

We can then define:

type ClosedLimit = 20
type Closed a = NClosed ClosedLimit a a

and sneak this constraint into the definition of universeGeneric:

universeGeneric :: (Generic a, GSmall (Rep a), Closed a) => [a]
universeGeneric = map to guniverse

(with an associated update to the default universe signature in class Small).

This separation between GClosed and NClosed allows us to indicate that non-generic Small instances are closed with a little boilerplate. For example, if we want to allow Word8's to be small:

instance Small Word8 where
  universe = universeEnum     -- use enum implementation
  type NClosed n a Int = ()   -- Word8s are closed

The full code looks like this:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.Generics
import Data.Kind
import GHC.TypeLits

type Closed a = NClosed ClosedLimit a a
type family GClosed n top f :: Constraint where
  GClosed 0 top f = TypeError (Text "Depth limit exceeded by type: " :<>: ShowType top)
  GClosed n top (M1 i c f) = GClosed n top f
  GClosed n top V1 = ()
  GClosed n top U1 = ()
  GClosed n top (f :+: g) = (GClosed n top f, GClosed n top g)
  GClosed n top (f :*: g) = (GClosed n top f, GClosed n top g)
  GClosed n top (K1 r a) = NClosed (n-1) top a
type ClosedLimit = 20

class Small a where
  universe :: [a]
  default universe :: (Generic a, GSmall (Rep a), Closed a) => [a]
  universe = universeGeneric
  type NClosed (n :: Nat) top a :: Constraint
  type instance NClosed n top a = GClosed n top (Rep a)

class GSmall f where
  guniverse :: [f p]

universeGeneric :: (Generic a, GSmall (Rep a), Closed a) => [a]
universeGeneric = map to guniverse

universeEnum :: (Bounded a, Enum a) => [a]
universeEnum = [minBound..maxBound]

instance GSmall f => GSmall (M1 i c f) where
  guniverse = map M1 guniverse
instance GSmall V1 where
  guniverse = []
instance GSmall U1 where
  guniverse = [U1]
instance (GSmall f, GSmall g) => GSmall (f :+: g) where
  guniverse = map L1 guniverse ++ map R1 guniverse
instance (GSmall f, GSmall g) => GSmall (f :*: g) where
  guniverse = [f :*: g | f <- guniverse, g <- guniverse]
instance Small a => GSmall (K1 r a) where
  guniverse = map K1 universe

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = Foo | Bar deriving (Show, Generic)

instance Small Route
instance Small BlogR

main = print $ universe @Route

Both of your "bad" examples are rejected. The first:

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = Post String deriving (Show, Generic)

generates a couple of nasty error messages about NClosed plus the reasonably friendly message:

No instance for (Small [Char])

Attempts to define instance Small [Char] will result in:

Depth limit exceeded by type: [Char]

while the second:

data Route = Index | Blog BlogR deriving (Show, Generic)
data BlogR = Foo | Bar | Rec Route deriving (Show, Generic)

generates the message:

Depth limit exceeded by type: Route

`Universe` - but for small and finite enumeration of ADTs

1 Answers