Last active
May 6, 2018 12:57
-
-
Save owickstrom/a427de11e9f6f34e6ba3e42ece3738c2 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- | 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