Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-- | This shows a way of computing a recursive type, and applying
-- constraints to individual types within it, using a type family.
-- I've commented the different parts, and the file ends with some
-- questions.
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module TypeFamilyConstraintsTuple where
import Data.Kind
import GHC.TypeLits
-- Let's say I have a library with 'MyOp' as part of the API, which
-- lets the user build a type-level list describing some data
-- structure (doesn't really matter what). I define a type for it, and
-- cute infix operators.
data MyOp = Symbol :+ Type | Symbol :- Type
infixl 6 :+
infixl 6 :-
-- Underpinning my library is another library, over which I do not
-- have control. It defines 'OtherOp', a type that recursively builds
-- up a description of a record data structure 'OtherRec' (it doesn't
-- in this code, but it's merely for illustrative purpose.)
data OtherOp
= Add Symbol Type OtherOp
| Remove Symbol Type OtherOp
| Noop
data OtherRec (o :: OtherOp)
-- Now I want to to compute an `OtherRec` type from my list of
-- `MyOp`s. For reasons that are hard to show in a short example I
-- need to constrain the types used in the resulting structure. Just
-- for illustrative purposes, I constrain them with 'Show' and 'Read'
-- in the following code. Anyhow, the following type family computes a
-- pair of an 'OtherOp' and a 'Constraint'. The constraints are
-- combined into a single constraint as it recurses through the
-- input list of 'MyOp's.
type family ToOtherOps (ms :: [MyOp]) (o :: OtherOp) (c :: Constraint) :: ( OtherOp, Constraint) where
ToOtherOps '[] o c = '(o, c)
ToOtherOps ((n :+ t) ': ms) o c = ToOtherOps ms (Add n t o) (c, Show t)
ToOtherOps ((n :- t) ': ms) o c = ToOtherOps ms (Remove n t o) (c, Read t)
-- Then I provide a handy type alias that unpacks the type family's
-- output tuple, and constrains the resulting the first element (a
-- type) using the second element (a constraint). 'Noop' is the
-- terminating type constructor for the other library's type.
type ToOtherRec ops =
forall t c.
( ToOtherOps ops Noop (() :: Constraint) ~ '(t, c)
, c
)
=> OtherRec t
-- Finally, I can convert my fancy list to the other library's structure:
type MyRec = ToOtherRec '["a" :+ String, "b" :+ Int, "a" :- String]
-- >>> :kind! MyRec
-- MyRec :: *
-- = ('('Remove "a" [Char] ('Add "b" Int ('Add "a" [Char] 'Noop)),
-- (((() :: Constraint, Show [Char]), Show Int), Read [Char]))
-- ~
-- '(t, c),
-- c) =>
-- OtherRec t
-- The reason I need to constrain types (Int and Char in this example)
-- in my actual project is that to extract those elements from the
-- underlying record data structure at a later point, and I need to
-- have constraints that witness that the elements are in there. That
-- is a consequence of how the row-types library works. See
-- https://hackage.haskell.org/package/row-types-0.2.0.0/docs/Data-Row-Records.html
-- for more details (if you are interested.)
--
-- Some questions:
--
-- * Are there any nicer ways of encoding this? Could this work with
-- multi-param type classes?
-- * Can I get rid of UndecidableInstances somehow?
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment