Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add IsSumType #133

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions generics-sop/src/Generics/SOP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,10 @@ module Generics.SOP (
, ProductCode
, productTypeFrom
, productTypeTo
, IsSumType
, SumCode
, sumTypeFrom
, sumTypeTo
, IsEnumType
, enumTypeFrom
, enumTypeTo
Expand Down
43 changes: 42 additions & 1 deletion generics-sop/src/Generics/SOP/Universe.hs
Original file line number Diff line number Diff line change
Expand Up @@ -185,6 +185,47 @@ productTypeTo :: IsProductType a xs => NP I xs -> a
productTypeTo = to . SOP . Z
{-# INLINE productTypeTo #-}

-- | Constraint that captures that a datatype is a (simple) sum type,
-- i.e., a type with some number of constructors, each of which
-- has a single argument.
--
-- It also gives access to the list of types which make up the union.
--
-- @since 0.5.2.0
--
type IsSumType (a :: Type) (xs :: [Type]) =
(Generic a, AllZip IsSingletonOf xs (Code a))

-- | Direct access to the list of types that makes up a sum type.
--
-- @since 0.5.2.0
--
type SumCode (a :: Type) = Heads (Code a)

-- | Convert from a sum type to its sum representation.
--
-- @since 0.5.2.0
--
sumTypeTo :: IsSumType a xs => a -> NS I xs
sumTypeTo = go . unSOP . from
where
go :: AllZip IsSingletonOf xs xss => NS (NP I) xss -> NS I xs
go (Z (x :* Nil)) = Z x
go (S xss) = S $ go xss
{-# INLINE sumTypeTo #-}

-- | Convert a sum representation to the original type.
--
-- @since 0.5.2.0
--
sumTypeFrom :: IsSumType a xs => NS I xs -> a
sumTypeFrom = to . SOP . go
where
go :: AllZip IsSingletonOf xs xss => NS I xs -> NS (NP I) xss
go (Z x) = Z (x :* Nil)
go (S xss) = S $ go xss
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd much rather have the conversion functions be applications of trans_NS.

This is simple enough for sumTypeFrom:

sumTypeFrom :: IsSumType a xs => a -> NS I xs
sumTypeFrom = to . SOP . trans_NS (Proxy :: Proxy IsSingletonOf) (:* Nil)

However, we need the flipped constraint for sumTypeTo:

sumTypeTo = trans_NS (Proxy :: Proxy (Flip IsSingletonOf)) hd . unSOP . from

This requires the obvious class/instance definition of Flip, but also means we have to add AllZip (Flip IsSingletonOf) (Code a) xs to the constraints for IsSumType.

This is a general annoyance with trans_NP and AllZip, the GHC cannot prove one constraint from the other. There are different options here:

  • add a version of AllZip that expands to both directions,
  • add a variant rtrans_* to the trans_* family of functions which works on the reversed constraint,
  • use explicit dictionary manipulation to turn one constraint into the other.

I'm not sure what's best.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I haven't forgotten about this, but it'll take me a while to try either of those, and I certainly don't feel like I have the judgement to say which of your suggested alternatives is better.

{-# INLINE sumTypeFrom #-}

-- | Constraint that captures that a datatype is an enumeration type,
-- i.e., none of the constructors have any arguments.
--
Expand All @@ -201,7 +242,7 @@ enumTypeFrom :: IsEnumType a => a -> NS (K ()) (Code a)
enumTypeFrom = map_NS (const (K ())) . unSOP . from
{-# INLINE enumTypeFrom #-}

-- | Convert a sum representation to ihe original type.
-- | Convert a enum representation to ihe original type.
--
enumTypeTo :: IsEnumType a => NS (K ()) (Code a) -> a
enumTypeTo = to . SOP . cmap_NS (Proxy :: Proxy ((~) '[])) (const Nil)
Expand Down
24 changes: 24 additions & 0 deletions generics-sop/test/Example.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,12 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-deprecations #-}
module Main (main, toTreeC, toDataFamC) where

Expand Down Expand Up @@ -206,6 +212,22 @@ instance Enumerable ABCC where
instance Enumerable VoidC where
enum = fmap toVoidC genumS

-- Use with derving via: much better than trying to write an overlapping
-- `(xs ~ SumCode a, IsSumType a xs, All Show xs) => Show a` instance
newtype AsSum a = AsSum a
instance (xs ~ SumCode a, IsSumType a xs, All Show xs) => Show (AsSum a) where
show (AsSum a) = go @xs $ sumTypeTo a
where
go :: (All Show xs') => NS I xs' -> String
go (Z (I x)) = show x
go (S xss) = go xss

data UnionType = C1 Tree | C2 TreeB
deriving stock (GHC.Generic)
-- Use anyclass deriving via GHC generics to fit this all in one deriving clause
deriving anyclass (Generic)
deriving Show via (AsSum UnionType)

-- Tests
main :: IO ()
main = do
Expand Down Expand Up @@ -238,3 +260,5 @@ main = do
print (voidDatatypeInfo == demotedVoidDatatypeInfo)
print (dataFamDatatypeInfo == demotedDataFamDatatypeInfo)
print $ convertFull tree
print $ C1 $ Leaf 1
print $ C2 $ LeafB 2
18 changes: 18 additions & 0 deletions sop-core/src/Data/SOP/Constraint.hs
Original file line number Diff line number Diff line change
Expand Up @@ -210,6 +210,16 @@ type family
type family Head (xs :: [a]) :: a where
Head (x ': xs) = x

-- We can't do this with a 'Map' family and 'Head' without unsaturated type families.

-- | Utility function to compute the heads of a type-level lists of type-level lists.
--
-- @since 0.5.2.0
--
type family Heads (xss :: [[k]]) :: [k] where
Heads '[] = '[]
Heads (x ': xs) = Head x ': Heads xs

-- | Utility function to compute the tail of a type-level list.
--
-- @since 0.3.1.0
Expand Down Expand Up @@ -284,3 +294,11 @@ type family AllZipN (h :: (k -> Type) -> (l -> Type)) (c :: k1 -> k2 -> Constrai
-- on whether the argument is indexed by a list or a list of lists.
--
type family SListIN (h :: (k -> Type) -> (l -> Type)) :: l -> Constraint

-- | Constraint that captures that a type-level list is a singleton of the given element.
--
-- This is a class rather than a type synonym so it can be passed as a type argument to types that take
-- a constraint, such as 'AllZip'.
--
class (as ~ '[a]) => IsSingletonOf (a :: k) (as :: [k])
instance (as ~ '[a]) => IsSingletonOf (a :: k) (as :: [k])