-- | Description : A short tutorial with code.
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module Data.OpenADT.Tutorial where
import Data.OpenADT
#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup ( (<>) )
#endif
-- row-types
import Data.Row
import Data.Row.Variants
-- recursion-schemes
import Data.Functor.Foldable ( Fix(..)
, cata
)
-- deriving-compat
import Text.Show.Deriving
import Data.Eq.Deriving
-- * Introduction
--
-- $introduction
-- This module demonstrates how to create open algebraic data types (ADT), and
-- is intended to be read top-to-bottom. Throughout this tutorial, we will
-- create two different list types, 'List1' and 'List2', that share two of
-- their constructors. We will also see various ways that our structures can be
-- traversed and modified.
--
-- Note that several extensions are used, which should show up in the Haddock
-- generated documentation. In particular, I recommend being familiar with
-- OverloadedLabels and TypeApplications, otherwise some syntax may be
-- confusing.
-- | A type alias to reduce typing when writing the types of algebras.
type Alg f x = f x -> x
-- * Constructors
--
-- $constructors
-- The first step is to create data types that correspond to the constructors
-- of the types we want. We create three different types corresponding to
-- three list constructors: 'NilF', 'Cons1F', 'Cons2F'.
--
-- For example, a two elements cons, 'Cons2F', is defined as:
--
-- @
-- -- | A two element cons element.
-- data Cons2F a x = Cons2F' a a x
-- deriving (Eq, Functor, Show)
-- @
--
-- Note that the recursion of the structure is expressed in the type variable
-- @x@ rather than explicitly. The constructor should also be a functor.
--
-- For convenience we can use 'deriveShow1' from "Text.Show.Deriving" to derive
-- 'Show1' instances (and 'deriveEq1' from "Data.Eq.Deriving" for 'Eq1' if
-- desired).
--
-- @
-- 'deriveShow1' ''Cons2F
-- @
-- | The base case of a list type.
data NilF x = NilF'
deriving (Eq, Functor, Show)
-- | A one element cons element.
data Cons1F a x = Cons1F' a x
deriving (Eq, Functor, Show)
-- | A two element cons element.
data Cons2F a x = Cons2F' a a x
deriving (Eq, Functor, Show)
deriveEq1 ''NilF
deriveEq1 ''Cons1F
deriveEq1 ''Cons2F
deriveShow1 ''NilF
deriveShow1 ''Cons1F
deriveShow1 ''Cons2F
-- * Rows
--
-- $rows
-- With constructors defined, we can define type synonyms that describe how
-- constructors are combined to create an ADT. These synonyms
-- are 'Row's, which are lists of labels (given by type-level strings) with
-- corresponding types. The type operator ('.==') is used to associate a label
-- with its type, the result of which is a row; ('.+') is used to combine two
-- rows into a new row. These operators, and the 'Row' type, are defined in
-- the row-types package.
-- | The row of the first list type. It defines a \"standard\" list type.
type List1RowF a = ( "nilF" .== NilF
.+ "cons1F" .== Cons1F a
)
-- | The row of the second list type. This type re-uses the constructors of
-- 'List1RowF' and includes a third constructor: a two element cons.
type List2RowF a = ( "nilF" .== NilF
.+ "cons1F" .== Cons1F a
.+ "cons2F" .== Cons2F a
)
-- * Types
--
-- $types
-- The 'VarF' newtype forms the basis of an open ADT. It wraps the variant
-- whose possible values are the constructors of the ADT. Its type constructor
-- takes two parameters:
--
-- - a row of types with the kind @(* -> *)@,
-- - and a type of kind @(*)@ that is applied to each element of the row.
--
-- 'VarF' has a functor instance when all the types of the row are functors.
-- Using 'VarF' we can define the base functor of our ADTs. Taking the fixpoint
-- of these functor types yields the ADT.
-- | The base functor of the 'List1' type. It is a 'VarF' with the row
-- 'List1RowF'.
type List1F a = VarF (List1RowF a)
-- | A list type. We obtain this type by taking the fixed point of its base
-- functor.
type List1 a = Fix (VarF (List1RowF a))
-- | The base functor of the 'List2' type.
type List2F a = VarF (List2RowF a)
-- | A list type with a two element cons. This type is defined with the
-- 'OpenADT' synonym, which is simply conveinience for @Fix (VarF r)@.
type List2 a = OpenADT (List2RowF a)
-- * Patterns
--
-- $patterns
-- In order to simplify our code, and avoid using 'VarF' directly, we can
-- define pattern synonyms for each constructor. Importantly, if written
-- generically enough, these patterns will work for a constructor regardless
-- the specific type it is used in. For example, we can write a single pattern
-- that matches the 'NilF' constructor in both the 'List1' and 'List2' types!
-- This is achieved with the pattern below:
--
-- @
-- pattern NilF :: (OpenAlg r "nilF" NilF x) => VarF r x
-- pattern NilF \<- VarF ('view' #nilF -\> Just NilF')
-- where NilF = VarF ('IsJust' #nilF NilF')
-- @
--
-- Note that in 'NilF', the variables @r@ and @x@ are left abstract. This
-- allows any row and type to be used with the pattern. In our
-- running example, @r@ could be either 'List1RowF' or 'List2RowF', while
-- @v@ could be either 'List1' or 'List2', respectively.
--
-- The pattern for the \"fixed\" constructor fixes the @x@ parameter to
-- @OpenADT r@ (below).
--
-- @
-- pattern Nil :: (OpenAlg r "nilF" NilF (OpenADT r)) => OpenADT r
-- pattern Nil = 'Fix' NilF
-- @
--
-- Since the patterns for each constructor are fairly repetative with only the
-- name changing, "Data.OpenADT.TH" provides a function, 'mkVarPattern', that
-- generates these patterns for you! The function takes four parameters:
--
-- 1. the type of the constructor,
-- 2. the label to be used for the constructor in the row,
-- 3. the name of the \"fixed\" pattern,
-- 4. and the name of the base functor pattern.
--
--
-- For example, the constructors for 'Cons1F' and 'Cons2F' can be created with:
--
-- @
-- mkVarPattern ''Cons1F \"cons1F\" \"Cons1\" \"Cons1F\"
-- mkVarPattern ''Cons2F \"cons2F\" \"Cons2\" \"Cons2F\"
-- @
pattern NilF :: (OpenAlg r "nilF" NilF x) => VarF r x
pattern NilF <- VarF (view #nilF -> Just NilF')
where NilF = VarF (IsJust #nilF NilF')
pattern Nil :: (OpenAlg r "nilF" NilF (OpenADT r)) => OpenADT r
pattern Nil = Fix NilF
mkVarPattern ''Cons1F "cons1F" "Cons1" "Cons1F"
mkVarPattern ''Cons2F "cons2F" "Cons2" "Cons2F"
-- * Constructing Values
--
-- $constructing
-- The patterns that we have written can be used to construct values as if they
-- were normal ADTs. The one caveat is that GHC cannot infer the types since
-- the variable @r@ in the patterns can be any row. This is, in practice, not
-- much of an issue as top-level type declarations are sufficient in most
-- cases.
--
-- For the remaining of this tutorial we will use the following lists in
-- examples:
--
-- @
-- exList1 :: List1 Int
-- exList1 = Cons1 0 (Cons1 1 Nil)
-- @
--
-- @
-- exList2 :: List2 Int
-- exList2 = Cons2 2 3 (Cons1 4 Nil)
-- @
-- | Construct a 'List1'. The patterns 'Cons1' and 'Nil' are used.
--
-- > >>> print exList1
-- > Fix (VarF (Cons1F' 0 (Fix (VarF (Cons1F' 1 (Fix (VarF NilF')))))))
exList1 :: List1 Int
exList1 = Cons1 0 (Cons1 1 Nil)
-- | Construct a 'List2'.
--
-- > >>> print exList2
-- > Fix (VarF (Cons2F' 2 3 (Fix (VarF (Cons1F' 4 (Fix (VarF NilF')))))))
exList2 :: List2 Int
exList2 = Cons2 2 3 (Cons1 4 Nil)
-- * Adding Constructors
--
-- $lifting
-- Adding constructors to an open ADT is easy. We can use 'cata' from the
-- recursion-schemes library to define a __cata__morphism (a bottom-up
-- traversal) over our ADT. At each node in our structure, we apply the
-- function 'diversifyF' (see also 'diversify'), which adds constructors to our
-- variant (without making any changes).
--
-- In the following example, a 'List1' is changed to a 'List2'. Note how the
-- type applications extension (-XTypeApplications) can be used to easily
-- specify the first type argument to 'diversifyF', which is the row the
-- variant is extended with.
--
-- @
-- result1 :: List2 Int
-- result1 = 'cata'
-- ('Fix' . 'diversifyF' \@(\"cons2F\" .== Cons2F Int)) exList1
-- @
-- | The constructor 'Cons2F' is added to 'exList1' without changing its
-- structure.
--
-- > >>> print result1
-- > Fix (VarF (Cons1F' 0 (Fix (VarF (Cons1F' 1 (Fix (VarF NilF')))))))
result1 :: List2 Int
result1 = cata
(Fix . diversifyF @("cons2F" .== Cons2F Int)) exList1
-- * Removing Constructors
--
-- $restricting
-- To convert an ADT of one type to another with /fewer/ constructors, we need
-- to specify how constructors are removed should they exist in the structure.
-- The function 'reduceVarF' removes the constructors in a structure
-- corresponding to the fields of the record ('Rec' from row-types) of its
-- first argument. This function may only be used to remove constructors; it
-- can not add or modify them. More specifically, it is constrained such that
-- the set of labels of the row of the input record must be exactly the set
-- of labels of the input 'VarF' /less/ the output 'VarF'. While more
-- constrained than strictly necessary, this allows GHC to infer types better.
-- Note in the example below that there are no annotations other than at the
-- top-level.
--
-- @
-- result2 :: List1 Int
-- result2 = 'cata' ('Fix' . 'reduceVarF' fns) exList2
-- where
-- fns = #cons2F .== \\(Cons2F' a b x) -> Cons1F a (Cons1 b x)
-- @
--
-- In the following sections we will see how to manipulate open ADT structures
-- more generally.
-- | Remove a constructor using 'reduceVarF' to convert a 'List2' to a 'List1'.
--
-- > >>> print result2
-- > Fix (VarF (Cons1F' 2 (Fix (VarF (Cons1F' 3 (Fix (VarF (Cons1F' 4 (Fix (VarF NilF'))))))))))
result2 :: List1 Int
result2 = cata (Fix . reduceVarF fns) exList2
where
fns = #cons2F .== \(Cons2F' a b x) -> Cons1F a (Cons1 b x)
-- * Pattern Matching
--
-- $matching
-- We previously used our constructor patterns to create structures, but the
-- patterns are bidirectional, so we can just as easily match with them. For
-- example, we can write a standard recursion scheme.
--
-- @
-- result3 :: List2 Int
-- result3 = 'cata' alg exList1
-- where
-- alg :: Alg (List1F Int) (List2 Int)
-- alg (Cons1F a x) = Cons2 a a x
-- alg NilF = Nil
-- alg _ = error
-- \"Unfortunately using these patterns will always result in non-\\\\
-- \\\\exhaustive pattern match errors, hence the default case. :(\"
-- @
--
-- Unfortunately, as noted in the default case of @alg@, GHC can not (does
-- not?) check the exhaustiveness of pattern synonyms. Using a default case
-- will get rid of non-exhaustiveness warnings, but could also hide bugs if it
-- is partial.
-- | Use \"traditional\" pattern matching to write an algebra over a 'List1'.
--
-- > >>> print result3
-- > Fix (VarF (Cons2F' 0 0 (Fix (VarF (Cons2F' 1 1 (Fix (VarF NilF')))))))
result3 :: List2 Int
result3 = cata alg exList1
where
alg :: Alg (List1F Int) (List2 Int)
alg (Cons1F a x) = Cons2 a a x
alg NilF = Nil
alg _ = error $
"Unfortunately using these patterns will always result in non-" <>
"exhaustive pattern match errors, hence the default case. :("
-- * Explicit Cases
--
-- $cases
-- An alternative that does not produce incomplete pattern warnings is to use
-- the 'caseonF' or 'switchF' functions (which are versions of 'caseon' and
-- 'switch' that operate on a 'VarF'). Similar to 'reduceVarF', these functions
-- require a record of functions that are then applied to the variant. However,
-- 'caseonF' and 'switchF' are more general than 'reduceVarF' in the sense that
-- the return type of the functions are not restricted. Note that the labels
-- and functions of the provided record must exactly match that of the input
-- type: no constructors may be omitted, nor is it possible to write any kind
-- of default case.
--
-- @
-- result4 :: List1 String
-- result4 = 'cata' ('caseonF' r) exList1
-- where r = #nilF .== (\\NilF' -> Nil)
-- .+ #cons1F .== (\\(Cons1F' a x) -> Cons1 (show \@Int a) x)
-- @
-- | An alternative way of writing 'result3' using 'caseonF'.
--
-- > >>> print result4
-- > Fix (VarF (Cons2F' 0 0 (Fix (VarF (Cons2F' 1 1 (Fix (VarF NilF')))))))
result4 :: List2 Int
result4 = cata (caseonF r) exList1
where r = #nilF .== (\NilF' -> Nil)
.+ #cons1F .== (\(Cons1F' a x) -> Cons2 a a x)
-- * A Type Class Approach
--
-- $classes
-- An alternative approach to direct pattern matching is using type classes to
-- define each case of an open ADT. The type class function can then be applied
-- to each value in an ADT recursively with 'cata' as we have seen before.
--
-- This approach is beneficial compared to direct pattern matching because the
-- compiler can find \"non-exhaustive matches\" in the form of missing
-- instances. Similar to patterns, the typeclasses are generic enough to work
-- on any open ADT type provided all of that type's constructors satisfy the
-- constraint.
--
-- Consider, for example, the following class that defines an operation for
-- modifying the contents of a list.
--
-- @
-- class OverList a a' r (f :: * -> *) where
-- fmapList' :: (a -> a') -> f (OpenADT r) -> OpenADT r
--
-- instance ( OpenAlg r "nilF" NilF (OpenADT r)) => OverList a a' r NilF where
-- fmapList' _ NilF' = Nil
--
-- instance ( OpenAlg r "cons1F" (Cons1F a') (OpenADT r)) => OverList a a' r (Cons1F a) where
-- fmapList' f (Cons1F' a x) = Cons1 (f a) x
--
-- instance ( OpenAlg r "cons2F" (Cons2F a') (OpenADT r)) => OverList a a' r (Cons2F a) where
-- fmapList' f (Cons2F' a b x) = Cons2 (f a) (f b) x
--
-- instance (Forall v (OverList a a' r)) => OverList a a' r (VarF v) where
-- fmapList' f = varFAlg \@(OverList a a' r) (fmapList' f)
-- @
--
-- The class 'OverList' has instances for all the constructors of 'List1' and
-- 'List2'. The final step is to recursively apply 'fmapList'' to the ADT.
--
-- @
-- fmapList f = 'cata' (fmapList' f)
-- @
--
-- The function 'varFAlg' is used to apply 'fmapList'' to a 'VarF'. As long as
-- all constructors satisfy the required constraint ('OverList' in this case),
-- we do not need to know the exact constructor.
--
-- Note that the type of 'fmapList' is polymorphic in its input and output
-- rows. Using 'fmapList', we can operate on both 'List1' and 'List2' types, or
-- any type that combines the three constructors that have 'OverList'
-- instances.
-- | This type class defines a fmap-like operation over lists.
class OverList a a' r (f :: * -> *) where
fmapList' :: (a -> a') -> f (OpenADT r) -> OpenADT r
instance ( OpenAlg r "nilF" NilF (OpenADT r)
) => OverList a a' r NilF where
fmapList' _ NilF' = Nil
instance ( OpenAlg r "cons1F" (Cons1F a') (OpenADT r)
) => OverList a a' r (Cons1F a) where
fmapList' f (Cons1F' a x) = Cons1 (f a) x
instance ( OpenAlg r "cons2F" (Cons2F a') (OpenADT r)
) => OverList a a' r (Cons2F a) where
fmapList' f (Cons2F' a b x) = Cons2 (f a) (f b) x
instance (Forall v (OverList a a' r)) => OverList a a' r (VarF v) where
fmapList' f = varFAlg @(OverList a a' r) (fmapList' f)
-- | Apply the 'fmapList'' function to any @(OpenADT r)@ provided all its
-- constructors satisfy the constraint @(OverList a a' s)@.
fmapList :: forall a a' r s.
( Forall r Functor
, Forall r (OverList a a' s)
)
=> (a -> a') -> OpenADT r -> OpenADT s
fmapList f = cata (fmapList' f)
-- | Demonstrate that 'fmapList' can be applied to 'exList1'.
--
-- > result5 = fmapList (show @Int) exList1 :: List1 String
--
-- > >>> print result5
-- > Fix (VarF (Cons1F' "0" (Fix (VarF (Cons1F' "1" (Fix (VarF NilF')))))))
result5 :: List1 String
result5 = fmapList (show @Int) exList1
-- | Demonstrate that 'fmapList' can be applied to 'exList2'.
--
-- > result6 = fmapList (show @Int) exList2 :: List2 String
--
-- > >>> print result6
-- > Fix (VarF (Cons2F' "2" "3" (Fix (VarF (Cons1F' "4" (Fix (VarF NilF')))))))
result6 :: List2 String
result6 = fmapList (show @Int) exList2
-- * Combining Explicit Cases and Type Classes
--
-- $cases2
-- Suppose we have an ADT where we want to operate on a subset of its
-- constructors. For example, a subset of constructors do not implement a type
-- class that the others do, or perhaps we just want to override a single
-- constructor while using some default implementation for the other cases.
-- These situations can be handled with the type class approach just discussed
-- with overlappable instances. Unfortunately, among other issues, we do not
-- receive compiler errors if we add a constructor but forget to write its
-- instance; the default instance automatically takes over.
--
-- Fortunately, we can use a combination of explicit cases and the type class
-- approach to prevent this from happening. The idea is to partition the ADT
-- variant and handle each set of constructors separately. To partition the
-- ADT, we can use 'multiTrialF' (see also 'multiTrial') one or more times.
--
-- @
-- result7 = 'cata' alg exList2 where
-- alg :: Alg (List2F Int) (List1 String)
-- alg w = case 'multiTrialF' \@("cons2F" .== Cons2F Int) w of
--
-- -- Explicit handling of specified constructors
-- Left v -> 'caseonF' r v
--
-- -- All others handled by fmapList'
-- Right leftovers -> 'fmapList'' (show \@Int) leftovers
--
-- r = #cons2F .== \\(Cons2F' a b x) ->
-- Cons1 ("(" <> show a <> " : " <> show b <> ")") x
-- @
-- | Demonstrate how to handle subsets of a 'VarF' individually.
--
-- Below is an alternate, but identical, implementation for the case where one
-- subset of variants matched is a single variant ('trialF' is used instead of
-- 'multiTrialF').
--
-- @
-- result7 = 'cata' alg exList2 where
-- alg w = case 'trialF' w #cons2F of
-- Left (Cons2F' a b x) -> Cons1 ("(" <> show a <> " : " <> show b <> ")") x
-- Right leftovers -> 'fmapList'' (show \@Int) leftovers
-- @
--
-- > >>> print result7
-- > Fix (VarF (Cons1F' "(2 : 3)" (Fix (VarF (Cons1F' "4" (Fix (VarF NilF')))))))
result7 :: List1 String
result7 = cata alg exList2 where
alg :: Alg (List2F Int) (List1 String)
alg w = case multiTrialF @("cons2F" .== Cons2F Int) w of
-- Explicit handling of specified constructors
Left v -> caseonF r v
-- All others handled by fmapList'
Right leftovers -> fmapList' (show @Int) leftovers
r = #cons2F .== \(Cons2F' a b x) ->
Cons1 ("(" <> show a <> " : " <> show b <> ")") x
-- | This is the function invoked by the executable in this package. It simply
-- prints out the examples.
main' :: IO ()
main' = do
putStrLn "exList1:"
print exList1
putStrLn "\nexList2:"
print exList2
putStrLn "\nresult1:"
print result1
putStrLn "\nresult2:"
print result2
putStrLn "\nresult3:"
print result3
putStrLn "\nresult4:"
print result4
putStrLn "\nresult5:"
print result5
putStrLn "\nresult6:"
print result6
putStrLn "\nresult7:"
print result7