HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Modulerow-types-1.0.1.2Haskell2010

Data.Row.Variants

This module implements extensible variants using closed type families.

  • 10 types
  • 4 classes
  • 38 values

Types and constraints

8 declarations
classclass KnownSymbol (n :: Symbol) where
#

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

datadata Var (r :: Row Type) where
#

The variant type.

Instances8AsConstructor', AsConstructor, Eq, Ord, Show, Generic, …
newtypenewtype Row a
#

The kind of rows. This type is only used as a datakind. A row is a typelevel entity telling us which symbols are associated with which types.

typetype Empty = 'R '[]
#

Type level version of empty

typetype (≈) (a :: k) (b :: k) = a ~ b
#

A lower fixity operator for type equality

Construction

6 declarations
classclass (r .! l) ≈ a => HasType (l :: Symbol) (a :: k) (r :: Row k)
#

Alias for (r .! l) ≈ a. It is a class rather than an alias, so that it can be partially applied.

Instances1HasType
  • (r .! l) ≈ a => HasType l a rDefined in row-types-1.0.1.2 · Data.Row.Internal
patternpattern IsJust :: (AllUniqueLabels r, KnownSymbol l) => Label l -> r .! l -> Var r
#

A pattern for variants; can be used to both destruct a variant when in a pattern position or construct one in an expression position.

Extension

familytype family (.\) (r :: Row k) (l :: Symbol) :: Constraint where
#

Does the row lack (i.e. it does not have) the specified label?

Equations

classclass Lacks (l :: Symbol) (r :: Row Type)
#

Alias for .\. It is a class rather than an alias, so that it can be partially applied.

Instances1Lacks
  • r .\ l => Lacks l rDefined in row-types-1.0.1.2 · Data.Row.Internal
familytype family (.\/) (l :: Row k) (r :: Row k) :: Row k where
#

The minimum join of the two rows.

Equations

  • (.\/) x ('R '[]) = x
  • (.\/) ('R '[]) y = y
  • (.\/) ('R l) ('R r) = 'R (MinJoinR l r)
familytype family (.+) (l :: Row k) (r :: Row k) :: Row k where
#

Type level Row append

Equations

Modification

valueupdate :: (KnownSymbol l, (r .! l) ≈ a) => Label l -> a -> Var r -> Var r
#

If the variant exists at the given label, update it to the given value. Otherwise, do nothing.

familytype family Modify (l :: Symbol) (a :: k) (r :: Row k) :: Row k where
#

Type level Row modification

Equations

  • Modify l a2 ('R ρ) = 'R (ModifyR l a2 ρ)

Destruction

8 declarations
valuetrial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l)
#

Convert a variant into either the value at the given label or a variant without that label. This is the basic variant destructor.

valueview :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
#

A convenient function for using view patterns when dispatching variants. For example:


 myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -> String
 myShow (view x -> Just n) = "Int of "++show n
 myShow (view y -> Just s) = "String of "++s

Types for destruction

familytype family (.!) (r :: Row k) (t :: Symbol) :: k where
#

Type level label fetching

Equations

  • (.!) ('R r) l = Get l r
familytype family (.-) (r :: Row k) (s :: Symbol) :: Row k where
#

Type level Row element removal

Equations

  • (.-) ('R r) l = 'R (Remove l r)
familytype family (.\\) (l :: Row k) (r :: Row k) :: Row k where
#

Type level Row difference. That is, l .\\ r is the row remaining after removing any matching elements of r from l.

Equations

  • (.\\) ('R l) ('R r) = 'R (Diff l r)
typetype (.==) (l :: Symbol) (a :: k) = Extend l a Empty
#

A type level way to create a singleton Row.

Native Conversion

7 declarations

The toNative and fromNative functions allow one to convert between Vars and regular Haskell data types ("native" types) that have the same number of constructors such that each constructor has one field and the same name as one of the options of the Var, which has the same type as that field. As expected, they compose to form the identity. Alternatively, one may use fromNativeGeneral, which allows a variant with excess options to still be transformed to a native type. Because of this, fromNativeGeneral requires a type application (although fromNative does not). The only requirement is that the native Haskell data type be an instance of Generic.

For example, consider the following simple data type:

Example1 expression
data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)

Then, we have the following:

Example2 expressions
toNative $ IsJust (Label @"Dog") 3 :: PetDog {age = 3}V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int){Dog=3}

Row operations

0 declarations

Map

familytype family Map (f :: a -> b) (r :: Row a) :: Row b where
#

Map a type level function over a Row.

Equations

  • Map f ('R r) = 'R (MapR f r)
valuemap :: Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
#

A function to map over a variant given a constraint.

valuemap' :: FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r)
#

A function to map over a variant given no constraint.

valuetransform
  1. :: Forall r c
  2. => forall (a1 :: a). c a1 => f a1 -> g a1
  3. -> Var (Map f r)
  4. -> Var (Map g r)
#

Lifts a natrual transformation over a variant. In other words, it acts as a variant transformer to convert a variant of f a values to a variant of g a values. If no constraint is needed, instantiate the first type argument with Unconstrained1.

Fold

classclass Forall (r :: Row k) (c :: k -> Constraint) where
#

Any structure over a row in which every element is similarly constrained can be metamorphized into another structure over the same row.

Instances2Forall
valueerase :: Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b
#

A standard fold

valueeraseZipGeneral
  1. :: (Forall ρ c, IsString s)
  2. => forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
  3. -> Var ρ
  4. -> Var ρ
  5. -> b
#

A fold over two variants at once. A call eraseZipGeneral f x y will return f (Left (show l, a, b)) when x and y both have values at the same label l and will return f (Right ((show l1, a), (show l2, b))) when they have values at different labels l1 and l2 respectively.

valueeraseZip
  1. :: Forall ρ c
  2. => forall a. c a => a -> a -> b
  3. -> Var ρ
  4. -> Var ρ
  5. -> Maybe b
#

A simpler fold over two variants at once

Applicative-like functions

Compose

We can easily convert between mapping two functors over the types of a row and mapping the composition of the two functors. The following two functions perform this composition with the gaurantee that:

Example1 expression
compose . uncompose = id
Example1 expression
uncompose . compose = id
valuecompose
  1. :: FreeForall r
  2. => Var (Map f (Map g r))
  3. -> Var (Map (Compose f g) r)
#

Convert from a variant where two functors have been mapped over the types to one where the composition of the two functors is mapped over the types.

valueuncompose
  1. :: FreeForall r
  2. => Var (Map (Compose f g) r)
  3. -> Var (Map f (Map g r))
#

Convert from a variant where the composition of two functors have been mapped over the types to one where the two functors are mapped individually one at a time over the types.

labels

ApSingle functions

valueeraseSingle
  1. :: Forall fs c
  2. => forall (f :: a -> Type). c f => f x -> y
  3. -> Var (ApSingle fs x)
  4. -> y
#

A version of erase that works even when the row-type of the variant argument is of the form ApSingle fs x.

valuemapSingle
  1. :: Forall fs c
  2. => forall (f :: a -> Type). c f => f x -> f y
  3. -> Var (ApSingle fs x)
  4. -> Var (ApSingle fs y)
#

Performs a functorial-like map over an ApSingle variant. In other words, it acts as a variant transformer to convert a variant of f x values to a variant of f y values. If no constraint is needed, instantiate the first type argument with Unconstrained1.

Coerce

valuecoerceVar :: BiForall r1 r2 Coercible => Var r1 -> Var r2
#

Coerce a variant to a coercible representation. The BiForall in the context indicates that the type of any option in r1 can be coerced to the type of the corresponding option in r2.

Internally, this is implemented just with unsafeCoerce, but we provide the following implementation as a proof:

newtype ConstV a b = ConstV { unConstV :: Var a }
newtype ConstV a b = FlipConstV { unFlipConstV :: Var b }
coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
coerceVar = unFlipConstV . biMetamorph @_ @_ @r1 @r2 @Coercible @Either @ConstV @FlipConstV @Const Proxy doNil doUncons doCons . ConstV
  where
    doNil = impossible . unConstV
    doUncons l = bimap ConstV Const . flip trial l . unConstV
    doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2, AllUniqueLabels (Extend ℓ τ2 ρ2))
           => Label ℓ -> Either (FlipConstV ρ1 ρ2) (Const τ1 τ2)
           -> FlipConstV (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
    doCons l (Left (FlipConstV v)) = FlipConstV $ extend @τ2 l v
    doCons l (Right (Const x)) = FlipConstV $ IsJust l (coerce @τ1 @τ2 x)
      \\ extendHas @ρ2 @ℓ @τ2