TypeFamilyConstraintsTuple.hs

-- | 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?