diff --git a/simplistic-generics.cabal b/simplistic-generics.cabal --- a/simplistic-generics.cabal +++ b/simplistic-generics.cabal @@ -1,33 +1,49 @@ -cabal-version: >=1.10 -name: simplistic-generics -version: 0.1.0.0 -synopsis: Generic programming without too many type classes -description: This library provides a representation build on top of - `GHC.Generics`, which can be used to describe generic - operations on a single function, instead of having - each case defined in an instance of a type class. --- bug-reports: -license: BSD3 -license-file: LICENSE -author: Alejandro Serrano -maintainer: trupill@gmail.com --- copyright: -category: Data -build-type: Simple -extra-source-files: README.md +cabal-version: 1.12 -library - exposed-modules: Generics.Simplistic, - Generics.Simplistic.Derive.Eq, - Generics.Simplistic.Derive.Functor, - Generics.Simplistic.Derive.Show - Data.Constraints - -- other-modules: - -- other-extensions: - build-depends: base >=4.12 && <5, kind-apply, comonad - hs-source-dirs: src - default-language: Haskell2010 +-- This file has been generated from package.yaml by hpack version 0.31.2. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 1b90926eead859c5af167c81f38f7e1fc252fdba35adaaad6ee34ae33b85009b +name: simplistic-generics +version: 2.0.0 +synopsis: Generic programming without too many type classes +description: This library provides a representation build on top of `GHC.Generics`, which can be used to describe generic operations on a single function, instead of having each case defined in an instance of a type class. +category: Data +author: Alejandro Serrano and Victor Miraldo +maintainer: trupill@gmail.com and v.cacciarimiraldo@gmail.com +license: BSD3 +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + source-repository head - type: git - location: https://gitlab.com/trupill/simplistic-generics + type: git + location: https://gitlab.com/trupill/simplistic-generics + +library + exposed-modules: + Generics.Simplistic + Generics.Simplistic.Deep + Generics.Simplistic.Deep.TH + Generics.Simplistic.Derive.Eq + Generics.Simplistic.Derive.Functor + Generics.Simplistic.Derive.Show + Generics.Simplistic.Unify + Generics.Simplistic.Util + Generics.Simplistic.Zipper + other-modules: + Paths_simplistic_generics + hs-source-dirs: + src/ + ghc-options: -O2 -Wall + build-depends: + base >=4.12 && <5 + , containers + , deepseq + , kind-apply + , mtl + , template-haskell + default-language: Haskell2010 diff --git a/src/Data/Constraints.hs b/src/Data/Constraints.hs deleted file mode 100644 --- a/src/Data/Constraints.hs +++ /dev/null @@ -1,16 +0,0 @@ -{-# language MultiParamTypeClasses, - UndecidableInstances, - QuantifiedConstraints, - ConstraintKinds, - FlexibleInstances, - KindSignatures, - PolyKinds #-} -module Data.Constraints where - -import GHC.Exts (Constraint) - -class (c => d) => Implies c d -instance (c => d) => Implies c d - -class Trivial c -instance Trivial c diff --git a/src/Generics/Simplistic.hs b/src/Generics/Simplistic.hs --- a/src/Generics/Simplistic.hs +++ b/src/Generics/Simplistic.hs @@ -1,63 +1,123 @@ -{-# language GADTs, - DataKinds, - PolyKinds, - TypeOperators, - ConstraintKinds, - MultiParamTypeClasses, - FlexibleContexts, - FlexibleInstances, - QuantifiedConstraints, - UndecidableInstances, - KindSignatures, - TypeFamilies #-} -module Generics.Simplistic ( - -- * From `GHC.Generics.Extra` module - Generic, Rep, Generic1, Rep1, - V1, U1, (:+:), (:*:), K1, M1, (:=>:), - -- * Simplistic representation on `*` types - SMeta(..), SRep(..), GenericSy, fromS, toS, fromI, toI, - -- ** Constraints over the leaves of a data type - OnLeaves, - -- * Simplistic representation on `* -> *` types - SRep1(..), GenericSy1, fromS1, toS1, +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +-- |Introduces closed representations functor +-- for "GHC.Generics" style generics. +module Generics.Simplistic + ( -- ** Re-exports from "GHC.Generics.Extra" module + Generic, Rep, Rep1, Par1, Rec1, (:.:)(..), V1, U1(..), (:+:)(..) + , (:*:)(..), K1(..), M1(..), (:=>:)(..), R + -- * Simplistic representation on @*@ types + , GMeta(..), SMeta(..), SMetaI(..), SRep(..) , I(..) , Simplistic -- ** Constraints over the leaves of a data type - OnLeaves1, + , OnLeaves + -- ** Combinators + -- *** Maps , zips and folds + , repMap , repMapM , repMapCM + , zipSRep , repLeaves , repLeavesC , repLeavesList + -- *** Metadata + , getDatatypeName , getConstructorName + , repDatatypeName , repConstructorName + -- ** Shallow Conversion + , fromS , toS , GShallow(..) + -- * Simplistic representation on @* -> *@ types + , SRep1(..) , OnLeaves1 , fromS1 , toS1 , GShallow1(..) , Simplistic1 -- * Auxiliary constraints - Implies, Trivial -) where + , Implies, Trivial + ) where -import Control.Comonad -import Data.Functor.Identity -import Data.Constraints +import Data.Proxy +import Control.Monad.Identity +import Control.DeepSeq + +import GHC.Generics import GHC.Generics.Extra import GHC.Exts (Constraint) +import Generics.Simplistic.Util + +--------------------- +-- Representations -- +--------------------- + data SMeta i t where SM_D :: Datatype d => SMeta D d SM_C :: Constructor c => SMeta C c SM_S :: Selector s => SMeta S s +deriving instance Show (SMeta i t) +deriving instance Eq (SMeta i t) +-- Dirty trick to access the dictionaries I need +data SMetaI d f x = SMetaI + +smetaI :: SMeta i t -> SMetaI t Proxy () +smetaI _ = SMetaI + +getDatatypeName :: SMeta D d -> String +getDatatypeName x@SM_D = datatypeName (smetaI x) + +getConstructorName :: SMeta C c -> String +getConstructorName x@SM_C = conName (smetaI x) + +-- |Singletons for metainformation +class GMeta i c where + smeta :: SMeta i c + +instance Constructor c => GMeta C c where + smeta = SM_C + +instance Datatype d => GMeta D d where + smeta = SM_D + +instance Selector s => GMeta S s where + smeta = SM_S + +-- |Given some @a@, a value of type @SRep w (Rep a)@ is +-- a closed representation of a generic value of type @a@. infixr 5 :**: data SRep w f where S_U1 :: SRep w U1 S_L1 :: SRep w f -> SRep w (f :+: g) S_R1 :: SRep w g -> SRep w (f :+: g) - (:**:) :: SRep w f -> SRep w g -> SRep w (f :*: g) + (:**:) :: SRep w f -> SRep w g -> SRep w (f :*: g) S_K1 :: w a -> SRep w (K1 i a) S_M1 :: SMeta i t -> SRep w f -> SRep w (M1 i t f) S_ST :: c => SRep w f -> SRep w (c :=>: f) - -type GenericSy a = (Generic a, Sy (Rep a)) +deriving instance (forall a. Show (w a)) => Show (SRep w f) +deriving instance (forall a. Eq (w a)) => Eq (SRep w f) +instance (forall x . NFData (w x)) => NFData (SRep w f) where + rnf S_U1 = () + rnf (S_K1 w) = rnf w + rnf (S_M1 _ x) = rnf x + rnf (S_L1 x) = rnf x + rnf (S_R1 x) = rnf x + rnf (x :**: y) = rnf x `seq` rnf y + rnf (S_ST x) = rnf x -fromS :: (GenericSy a, Applicative w) => a -> SRep w (Rep a) -fromS = fromS' . from -fromI :: (GenericSy a) => a -> SRep Identity (Rep a) -fromI = fromS -toS :: (GenericSy a, Comonad w) => SRep w (Rep a) -> a -toS = to . toS' -toI :: (GenericSy a) => SRep Identity (Rep a) -> a -toI = toS +-- |All types supported by "GHC.Generics" are /simplistic/, this +-- constraint just couples their necessary together. +type Simplistic a = (Generic a , GShallow (Rep a)) +-- |Computes the constraint that corresponds to ensuring all +-- leaves of a representation satisfy a given constraint. +-- For example, +-- +-- > OnLeaves Eq (Rep (Either a b)) = (Eq a , Eq b) +-- type family OnLeaves (c :: * -> Constraint) (f :: * -> *) :: Constraint where OnLeaves c V1 = () OnLeaves c U1 = () @@ -67,7 +127,202 @@ OnLeaves c (M1 i p f) = OnLeaves c f OnLeaves c (d :=>: f) = Implies d (OnLeaves c f) +-- |Retrieves the datatype name for a representation. +-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of +-- a type constructed with "GHC.Generics" builtin mechanisms. +repDatatypeName :: SRep w f -> String +repDatatypeName (S_M1 x@SM_D _) + = getDatatypeName x +repDatatypeName (S_M1 _ x) + = repDatatypeName x +repDatatypeName (S_L1 x) + = repDatatypeName x +repDatatypeName (S_R1 x) + = repDatatypeName x +repDatatypeName _ + = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep" + +-- |Retrieves the constructor name for a representation. +-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of +-- a type constructed with "GHC.Generics" builtin mechanisms. +repConstructorName :: SRep w f -> String +repConstructorName (S_M1 x@SM_C _) + = getConstructorName x +repConstructorName (S_M1 _ x) + = repConstructorName x +repConstructorName (S_L1 x) + = repConstructorName x +repConstructorName (S_R1 x) + = repConstructorName x +repConstructorName _ + = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep" + +-- |Zips two representations together if they are made up of +-- the same constructor. For example, +-- +-- > zipSRep (fromS (: 1 [])) (fromS (: 2 (: 3 []))) +-- > == Just (fromS (: (1 , 2) ([] , [3]))) +-- > +-- > zipSRep (fromS (: 1 [])) (fromS []) +-- > == Nothing +zipSRep :: SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f) +zipSRep S_U1 S_U1 = return S_U1 +zipSRep (S_L1 x) (S_L1 y) = S_L1 <$> zipSRep x y +zipSRep (S_R1 x) (S_R1 y) = S_R1 <$> zipSRep x y +zipSRep (S_M1 m x) (S_M1 _ y) = S_M1 m <$> zipSRep x y +zipSRep (x1 :**: x2) (y1 :**: y2) = (:**:) <$> (zipSRep x1 y1) <*> (zipSRep x2 y2) +zipSRep (S_K1 x) (S_K1 y) = return $ S_K1 (x :*: y) +zipSRep _ _ = Nothing + +-- |Performs a /crush/ over the leaves of a 'SRep' carrying a constraint +-- around. +repLeavesC :: (OnLeaves c rep) + => Proxy c + -> (forall x . c x => w x -> r) -- ^ leaf extraction + -> (r -> r -> r) -- ^ join product + -> r -- ^ empty + -> SRep w rep -> r +repLeavesC _ _ _ e S_U1 = e +repLeavesC p l j e (S_L1 x) = repLeavesC p l j e x +repLeavesC p l j e (S_R1 x) = repLeavesC p l j e x +repLeavesC p l j e (S_M1 _ x) = repLeavesC p l j e x +repLeavesC p l j e (x :**: y) = j (repLeavesC p l j e x) (repLeavesC p l j e y) +repLeavesC _ l _ _ (S_K1 x) = l x +repLeavesC p l j e (S_ST x) = repLeavesC p l j e x + + +-- |Performs a /crush/ over the leaves of a 'SRep' +repLeaves :: (forall x . w x -> r) -- ^ leaf extraction + -> (r -> r -> r) -- ^ join product + -> r -- ^ empty + -> SRep w rep -> r +repLeaves _ _ e S_U1 = e +repLeaves l j e (S_L1 x) = repLeaves l j e x +repLeaves l j e (S_R1 x) = repLeaves l j e x +repLeaves l j e (S_M1 _ x) = repLeaves l j e x +repLeaves l j e (x :**: y) = j (repLeaves l j e x) (repLeaves l j e y) +repLeaves l _ _ (S_K1 x) = l x +repLeaves l j e (S_ST x) = repLeaves l j e x + +-- |Example of 'repLeaves' that places the values of @w@ inside +-- a list. +repLeavesList :: SRep w rep -> [Exists w] +repLeavesList = repLeaves ((:[]) . Exists) (++) [] + +-- |Maps a function over a representation taking into +-- account that the leaves of the representation satisfy +-- a given constraint. +repMapCM :: (Monad m , OnLeaves c rep) + => Proxy c -- ^ Which constraint shall be threaded through + -> (forall y . c y => f y -> m (g y)) + -> SRep f rep -> m (SRep g rep) +repMapCM _p _f (S_U1) = return S_U1 +repMapCM _p f (S_K1 x) = S_K1 <$> f x +repMapCM p f (S_M1 m x) = S_M1 m <$> repMapCM p f x +repMapCM p f (S_L1 x) = S_L1 <$> repMapCM p f x +repMapCM p f (S_R1 x) = S_R1 <$> repMapCM p f x +repMapCM p f (x :**: y) = (:**:) <$> repMapCM p f x <*> repMapCM p f y +repMapCM p f (S_ST x) = S_ST <$> repMapCM p f x + +-- |Maps a monadic function over the representation +repMapM :: (Monad m) + => (forall y . f y -> m (g y)) + -> SRep f rep -> m (SRep g rep) +repMapM _f (S_U1) = return S_U1 +repMapM f (S_K1 x) = S_K1 <$> f x +repMapM f (S_M1 m x) = S_M1 m <$> repMapM f x +repMapM f (S_L1 x) = S_L1 <$> repMapM f x +repMapM f (S_R1 x) = S_R1 <$> repMapM f x +repMapM f (S_ST x) = S_ST <$> repMapM f x +repMapM f (x :**: y) + = (:**:) <$> repMapM f x <*> repMapM f y + +-- |Maps a simple functino over the representation +repMap :: (forall y . f y -> g y) + -> SRep f rep -> SRep g rep +repMap f = runIdentity . repMapM (return . f) + +-------------------------------- + +-- |Identity functor +newtype I x = I { unI :: x } + deriving Eq + +instance Show x => Show (I x) where + showsPrec p (I x) = showParen (p > 10) $ showString "I " . showsPrec 11 x +instance Functor I where + fmap f (I x) = I (f x) +instance Applicative I where + pure = I + I f <*> I x = I (f x) +instance Monad I where + I x >>= f = f x + +-- |Shallow conversion between "GHC.Generics" representation +-- and 'SRep'; The 'fromS' and 'toS' functions provide the +-- toplevel api. +class GShallow f where + sfrom :: f x -> SRep I f + sto :: SRep I f -> f x + +instance GShallow U1 where + sfrom U1 = S_U1 + sto S_U1 = U1 + +instance (GShallow f , GShallow g) => GShallow (f :+: g) where + sfrom (L1 x) = S_L1 (sfrom x) + sfrom (R1 x) = S_R1 (sfrom x) + sto (S_L1 x) = L1 (sto x) + sto (S_R1 x) = R1 (sto x) + +instance (GShallow f , GShallow g) => GShallow (f :*: g) where + sfrom (x :*: y) = sfrom x :**: sfrom y + sto (x :**: y) = sto x :*: sto y + +instance (GShallow f , GMeta i c) => GShallow (M1 i c f) where + sfrom (M1 x) = S_M1 smeta (sfrom x) + sto (S_M1 _ x) = M1 (sto x) + +instance GShallow (K1 R x) where + sfrom (K1 x) = S_K1 (I x) + sto (S_K1 (I x)) = K1 x + +-- |Converts a value of a generic type directly to its +-- (shallow) simplistic representation. +fromS :: (Simplistic a) => a -> SRep I (Rep a) +fromS = sfrom . from + +-- |Converts a simplistic representation back to its corresponding +-- value of type @a@. +toS :: (Simplistic a) => SRep I (Rep a) -> a +toS = to . sto + +-- TODO: Study whether it makes sense to add rules +-- and inline pragmas for performance. +-- {-# RULES "sfrom/sto" forall x. sfrom (sto x) = x #-} +-- {-# RULES "sto/sfrom" forall x. sto (sfrom x) = x #-} + +--------------------------------------- +--------------------------------------- +-- Representation of `* -> *` types -- +--------------------------------------- +--------------------------------------- + +-- $simplistic1 +-- +-- "GHC.Generics" provides 'Rep' for types of kind @*@ +-- and 'Rep1' for types of kind @* -> *@. Similarly, +-- we also provide 'SRep1' for a closed-universe interpretation +-- of 'Rep1'. It is worth noting the support is limitted and +-- we have not yet written combinators for 'SRep1' like we +-- did for 'SRep'. An example usage of 'SRep1' can be found +-- in "Generics.Simplistic.Derive.Functor". + infixr 5 :***: + +-- |Similar to 'SRep', but is indexed over the functors that +-- make up a 'Rep1', used to explicitely encode types with +-- one parameter. data SRep1 f x where S1_U1 :: SRep1 U1 x S1_L1 :: SRep1 f x -> SRep1 (f :+: g) x @@ -80,12 +335,7 @@ S1_Rec :: f x -> SRep1 (Rec1 f) x S1_Comp :: f (SRep1 g x) -> SRep1 (f :.: g) x -type GenericSy1 f = (Generic1 f, Sy1 (Rep1 f)) - -fromS1 :: (GenericSy1 f) => f a -> SRep1 (Rep1 f) a -fromS1 = fromS1' . from1 -toS1 :: (GenericSy1 f) => SRep1 (Rep1 f) a -> f a -toS1 = to1 . toS1' +type Simplistic1 f = (Generic1 f, GShallow1 (Rep1 f)) type family OnLeaves1 (c :: * -> Constraint) (r :: (* -> *) -> Constraint) (f :: * -> *) :: Constraint where @@ -100,74 +350,48 @@ OnLeaves1 c r (Rec1 f) = r f OnLeaves1 c r (f :.: g) = (r f, OnLeaves1 c r g) --- Internal instances -class SMety i t where - smeta :: SMeta i t -instance Datatype d => SMety D d where - smeta = SM_D -instance Constructor c => SMety C c where - smeta = SM_C -instance Selector s => SMety S s where - smeta = SM_S -class Sy f where - fromS' :: Applicative w => f a -> SRep w f - toS' :: Comonad w => SRep w f -> f a -instance Sy V1 where - fromS' = undefined - toS' = undefined -instance Sy U1 where - fromS' U1 = S_U1 - toS' S_U1 = U1 -instance (Sy f, Sy g) => Sy (f :+: g) where - fromS' (L1 x) = S_L1 (fromS' x) - fromS' (R1 y) = S_R1 (fromS' y) - toS' (S_L1 x) = L1 (toS' x) - toS' (S_R1 y) = R1 (toS' y) -instance (Sy f, Sy g) => Sy (f :*: g) where - fromS' (x :*: y) = fromS' x :**: fromS' y - toS' (x :**: y) = toS' x :*: toS' y -instance Sy (K1 i a) where - fromS' (K1 x) = S_K1 (pure x) - toS' (S_K1 x) = K1 (extract x) -instance (SMety i t, Sy f) => Sy (M1 i t f) where - fromS' (M1 x) = S_M1 smeta (fromS' x) - toS' (S_M1 _ x) = M1 (toS' x) -instance (c => Sy f) => Sy (c :=>: f) where - fromS' (SuchThat x) = S_ST (fromS' x) - toS' (S_ST x) = SuchThat (toS' x) +-- |Converts a value of a generic type directly to its +-- (shallow) simplistic1 representation with a parameter. +fromS1 :: (Simplistic1 f) => f x -> SRep1 (Rep1 f) x +fromS1 = sfrom1 . from1 -class Sy1 f where - fromS1' :: f a -> SRep1 f a - toS1' :: SRep1 f a -> f a -instance Sy1 V1 where - fromS1' = undefined - toS1' = undefined -instance Sy1 U1 where - fromS1' U1 = S1_U1 - toS1' S1_U1 = U1 -instance (Sy1 f, Sy1 g) => Sy1 (f :+: g) where - fromS1' (L1 x) = S1_L1 (fromS1' x) - fromS1' (R1 y) = S1_R1 (fromS1' y) - toS1' (S1_L1 x) = L1 (toS1' x) - toS1' (S1_R1 y) = R1 (toS1' y) -instance (Sy1 f, Sy1 g) => Sy1 (f :*: g) where - fromS1' (x :*: y) = fromS1' x :***: fromS1' y - toS1' (x :***: y) = toS1' x :*: toS1' y -instance Sy1 (K1 i a) where - fromS1' (K1 x) = S1_K1 x - toS1' (S1_K1 x) = K1 x -instance (SMety i t, Sy1 f) => Sy1 (M1 i t f) where - fromS1' (M1 x) = S1_M1 smeta (fromS1' x) - toS1' (S1_M1 _ x) = M1 (toS1' x) -instance (c => Sy1 f) => Sy1 (c :=>: f) where - fromS1' (SuchThat x) = S1_ST (fromS1' x) - toS1' (S1_ST x) = SuchThat (toS1' x) -instance Sy1 Par1 where - fromS1' (Par1 x) = S1_Par x - toS1' (S1_Par x) = Par1 x -instance Sy1 (Rec1 f) where - fromS1' (Rec1 x) = S1_Rec x - toS1' (S1_Rec x) = Rec1 x -instance (Functor f, Sy1 g) => Sy1 (f :.: g) where - fromS1' (Comp1 x) = S1_Comp (fmap fromS1' x) - toS1' (S1_Comp x) = Comp1 (fmap toS1' x) +-- |Converts a simplistic1 representation back to its corresponding +-- value of type @a@. +toS1 :: (Simplistic1 f) => SRep1 (Rep1 f) x -> f x +toS1 = to1 . sto1 + +class GShallow1 f where + sfrom1 :: f a -> SRep1 f a + sto1 :: SRep1 f a -> f a +instance GShallow1 V1 where + sfrom1 = undefined + sto1 = undefined +instance GShallow1 U1 where + sfrom1 U1 = S1_U1 + sto1 S1_U1 = U1 +instance (GShallow1 f, GShallow1 g) => GShallow1 (f :+: g) where + sfrom1 (L1 x) = S1_L1 (sfrom1 x) + sfrom1 (R1 y) = S1_R1 (sfrom1 y) + sto1 (S1_L1 x) = L1 (sto1 x) + sto1 (S1_R1 y) = R1 (sto1 y) +instance (GShallow1 f, GShallow1 g) => GShallow1 (f :*: g) where + sfrom1 (x :*: y) = sfrom1 x :***: sfrom1 y + sto1 (x :***: y) = sto1 x :*: sto1 y +instance GShallow1 (K1 i a) where + sfrom1 (K1 x) = S1_K1 x + sto1 (S1_K1 x) = K1 x +instance (GMeta i t, GShallow1 f) => GShallow1 (M1 i t f) where + sfrom1 (M1 x) = S1_M1 smeta (sfrom1 x) + sto1 (S1_M1 _ x) = M1 (sto1 x) +instance (c => GShallow1 f) => GShallow1 (c :=>: f) where + sfrom1 (SuchThat x) = S1_ST (sfrom1 x) + sto1 (S1_ST x) = SuchThat (sto1 x) +instance GShallow1 Par1 where + sfrom1 (Par1 x) = S1_Par x + sto1 (S1_Par x) = Par1 x +instance GShallow1 (Rec1 f) where + sfrom1 (Rec1 x) = S1_Rec x + sto1 (S1_Rec x) = Rec1 x +instance (Functor f, GShallow1 g) => GShallow1 (f :.: g) where + sfrom1 (Comp1 x) = S1_Comp (fmap sfrom1 x) + sto1 (S1_Comp x) = Comp1 (fmap sto1 x) diff --git a/src/Generics/Simplistic/Deep.hs b/src/Generics/Simplistic/Deep.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Simplistic/Deep.hs @@ -0,0 +1,390 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UndecidableSuperClasses #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-orphans #-} +-- |Deep representation for 'SRep' +module Generics.Simplistic.Deep + ( -- * (Co)Free (Co)Monad and its cousins + HolesAnn(..) + , SFix , pattern SFix , pattern Prim + , SFixAnn , pattern SFixAnn , pattern PrimAnn + , Holes , pattern Roll , pattern Hole + -- ** Constraints + , CompoundCnstr , PrimCnstr + -- ** Coercions + , holesToSFix , sfixToHoles + -- ** Maps, zips and folds + , holesMapAnn , holesMap , holesMapM , holesMapAnnM , getAnn + , holesJoin , holesSize, holesHolesList + , holesRefineM , holesRefineHoles , holesRefineHolesM + , synthesize , synthesizeM , cataM + -- ** Anti-Unification + , lgg + -- ** Conversion + , Deep(..) , GDeep(..) + ) where + +import Data.Proxy +-- import qualified Data.Set as S (Set, fromList) +import Control.Monad.Identity +import Control.DeepSeq +import GHC.Generics (from , to) +import Unsafe.Coerce + +import Generics.Simplistic +import Generics.Simplistic.Util + +-- Useful constraints + +type PrimCnstr kappa fam b + = (Elem b kappa , NotElem b fam) + +type CompoundCnstr kappa fam a + = (Elem a fam , NotElem a kappa , Generic a) + +-- |The cofree comonad and free monad on the same type; +-- this allows us to use the same recursion operator +-- for everything. +data HolesAnn kappa fam ann h a where + Hole' :: ann a -- ^ Annotation + -> h a -> HolesAnn kappa fam ann h a + Prim' :: (PrimCnstr kappa fam a) + => ann a -- ^ Annotation + -> a -> HolesAnn kappa fam ann h a + Roll' :: (CompoundCnstr kappa fam a) + => ann a -- ^ Annotation + -> SRep (HolesAnn kappa fam ann h) (Rep a) + -> HolesAnn kappa fam ann h a + +instance (All Eq kappa , EqHO h) => EqHO (Holes kappa fam h) where + eqHO x y = all (exElim $ uncurry' go) $ holesHolesList (lgg x y) + where + go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool + go (Hole h1) (Hole h2) = eqHO h1 h2 + go _ _ = False + +instance (All Eq kappa , EqHO h) => Eq (Holes kappa fam h t) where + (==) = eqHO + +-- |Deep representations are easily achieved by forbiding +-- the 'Hole'' constructor and providing unit annotations. +type SFix kappa fam = HolesAnn kappa fam U1 V1 + +pattern SFix :: () => (CompoundCnstr kappa fam a) + => SRep (SFix kappa fam) (Rep a) + -> SFix kappa fam a +pattern SFix x = Roll x +{-# COMPLETE SFix , Prim #-} + +-- |A tree with holes has unit annotations +type Holes kappa fam = HolesAnn kappa fam U1 + +pattern Hole :: h a -> Holes kappa fam h a +pattern Hole x = Hole' U1 x + +pattern Prim :: () => (PrimCnstr kappa fam a) + => a -> Holes kappa fam h a +pattern Prim a = Prim' U1 a + +pattern Roll :: () => (CompoundCnstr kappa fam a) + => SRep (Holes kappa fam h) (Rep a) + -> Holes kappa fam h a +pattern Roll x = Roll' U1 x +{-# COMPLETE Hole , Prim , Roll #-} + +-- |Annotated fixpoints are also easy; forbid the 'Hole'' +-- constructor but add something to every 'Roll' of +-- the representation. +type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1 + +pattern PrimAnn :: () => (PrimCnstr kappa fam a) + => ann a -> a -> SFixAnn kappa fam ann a +pattern PrimAnn ann a = Prim' ann a + +pattern SFixAnn :: () => (CompoundCnstr kappa fam a) + => ann a + -> SRep (SFixAnn kappa fam ann) (Rep a) + -> SFixAnn kappa fam ann a +pattern SFixAnn ann x = Roll' ann x +{-# COMPLETE SFixAnn , PrimAnn #-} + +--------------- +-- Coercions -- +--------------- + +sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at +sfixToHoles = unsafeCoerce + +holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at +holesToSFix = id + +------------ +-- NFData -- +------------ + +-- VCM: QUESTION: DDoes it make sense to have this here? +-- I need it in /hdiff/, and I can see how it can be useful. +-- @trupill, do you prefer to keep this or trash this? + +instance (forall x . NFData (ann x) , forall x . NFData (h x)) + => NFData (HolesAnn kappa fam ann h f) where + rnf (Prim' ann _) = rnf ann + rnf (Hole' ann h) = rnf ann `seq` rnf h + rnf (Roll' ann x) = rnf ann `seq` rnf x + +instance NFData (V1 x) where + rnf _ = () + +instance NFData (U1 x) where + rnf U1 = () + +---------------------- +-- Useful Functions -- +---------------------- + +-- |Retrieves the annotation inside a 'HolesAnn'; +-- this is the counit of the comonad. +getAnn :: HolesAnn kappa fam ann h a -> ann a +getAnn (Hole' ann _) = ann +getAnn (Prim' ann _) = ann +getAnn (Roll' ann _) = ann + +-- TODO: swap parameters +-- |Maps over a 'HolesAnn' treating annotations and holes +-- independently. +holesMapAnnM :: (Monad m) + => (forall x . f x -> m (g x)) -- ^ Function to transform holes + -> (forall x . ann x -> m (psi x)) -- ^ Function to transform annotations + -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam psi g a) +holesMapAnnM f g (Hole' a x) = Hole' <$> g a <*> f x +holesMapAnnM _ g (Prim' a x) = flip Prim' x <$> g a +holesMapAnnM f g (Roll' a x) = Roll' <$> g a <*> repMapM (holesMapAnnM f g) x + +-- |Maps over 'HolesAnn' maintaining annotations intact. +holesMapM :: (Monad m) + => (forall x . f x -> m (g x)) + -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a) +holesMapM f = holesMapAnnM f return + +-- |Maps over the holes in a 'HolesAnn' +holesMap :: (forall x . f x -> g x) + -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a +holesMap f = runIdentity . holesMapM (return . f) + +-- |Maps over holes and annotations in a 'HolesAnn' +holesMapAnn :: (forall x . f x -> g x) + -> (forall x . ann x -> phi x) + -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam phi g a +holesMapAnn f g = runIdentity . holesMapAnnM (return . f) (return . g) + +-- |Monadic multiplication +holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a + -> HolesAnn kappa fam ann f a +holesJoin (Hole' _ x) = x +holesJoin (Prim' a x) = Prim' a x +holesJoin (Roll' a x) = Roll' a (repMap holesJoin x) + +-- |Computes the list of holes in a 'HolesAnn' +holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f] +holesHolesList (Hole' _ x) = [Exists x] +holesHolesList (Prim' _ _) = [] +holesHolesList (Roll' _ x) = concatMap (exElim holesHolesList) $ repLeavesList x + +{- +holesHolesSet :: (Ord (Exists f)) => Holes kappa fam f a -> S.Set (Exists f) +holesHolesSet = S.fromList . holesHolesList +-} + +-- TODO: Implement holesMap in terms of refine; its much better! + +-- |Refines holes using a monadic action +holesRefineHolesM :: (Monad m) + => (forall b . f b -> m (Holes kappa fam g b)) + -> Holes kappa fam f a + -> m (Holes kappa fam g a) +holesRefineHolesM f = fmap holesJoin . holesMapM f + +-- |Refine holes with a simple action +holesRefineHoles :: (forall b . f b -> Holes kappa fam g b) + -> Holes kappa fam f a + -> Holes kappa fam g a +holesRefineHoles f = holesJoin . runIdentity . holesMapM (return . f) + +-- |Refine holes and primitives +holesRefineM :: (Monad m) + => (forall b . f b -> m (Holes kappa fam g b)) + -> (forall b . (PrimCnstr kappa fam b) + => b -> m (Holes kappa fam g b)) + -> Holes kappa fam f a + -> m (Holes kappa fam g a) +holesRefineM f _ (Hole x) = f x +holesRefineM _ g (Prim x) = g x +holesRefineM f g (Roll x) = Roll <$> repMapM (holesRefineM f g) x + +-- |Counts how many 'Prim's and 'Roll's are inside a 'HolesAnn'. +holesSize :: HolesAnn kappa fam ann h a -> Int +holesSize (Hole' _ _) = 0 +holesSize (Prim' _ _) = 1 +holesSize (Roll' _ x) = 1 + sum (map (exElim holesSize) $ repLeavesList x) + +-- |Catamorphism over 'HolesAnn' +cataM :: (Monad m) + => (forall b . (CompoundCnstr kappa fam b) + => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion + -> (forall b . (PrimCnstr kappa fam b) + => ann b -> b -> m (phi b)) -- ^ How to handle primitivies + -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes + -> HolesAnn kappa fam ann h a + -> m (phi a) +cataM f g h (Roll' ann x) = repMapM (cataM f g h) x >>= f ann +cataM _ g _ (Prim' ann x) = g ann x +cataM _ _ h (Hole' ann x) = h ann x + +-- |Synthetization of attributes +synthesizeM :: (Monad m) + => (forall b . (CompoundCnstr kappa fam b) + => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion + -> (forall b . (PrimCnstr kappa fam b) + => ann b -> b -> m (phi b)) -- ^ How to handle primitives + -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes + -> HolesAnn kappa fam ann h a + -> m (HolesAnn kappa fam phi h a) +synthesizeM f g h = cataM (\ann r -> flip Roll' r + <$> f ann (repMap getAnn r)) + (\ann b -> flip Prim' b <$> g ann b) + (\ann r -> flip Hole' r <$> h ann r) + +-- |Simpler version of 'synthesizeM' working over the /Identity/ monad. +synthesize :: (forall b . (CompoundCnstr kappa fam b) + => ann b -> SRep phi (Rep b) -> phi b) + -> (forall b . (PrimCnstr kappa fam b) + => ann b -> b -> phi b) + -> (forall b . ann b -> h b -> phi b) + -> HolesAnn kappa fam ann h a + -> HolesAnn kappa fam phi h a +synthesize f g h = runIdentity + . synthesizeM (\ann -> return . f ann) + (\ann -> return . g ann) + (\ann -> return . h ann) + +-- Anti unification is so simple it doesn't +-- deserve its own module + +-- |Computes the /least general generalization/ of two +-- trees. +lgg :: forall kappa fam h i a + . (All Eq kappa) + => Holes kappa fam h a -> Holes kappa fam i a + -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a +lgg (Prim x) (Prim y) + | weq (Proxy :: Proxy kappa) x y = Prim x + | otherwise = Hole (Prim x :*: Prim y) +lgg x@(Roll rx) y@(Roll ry) = + case zipSRep rx ry of + Nothing -> Hole (x :*: y) + Just r -> Roll (repMap (uncurry' lgg) r) +lgg x y = Hole (x :*: y) + +---------------------- +-- Deep translation -- +---------------------- + +{- It is possible to have a simler GDeep; relying on +-- GShallow. I'll test performance later. + +class GDeep' fam prim isPrim a where + gdfrom' :: Proxy isPrim -> a -> SFix fam prim a + gdto' :: Proxy isPrim -> SFix fam prim a -> a + +instance (CompoundCnstr fam prim a , GDeep fam prim a) + => GDeep' fam prim 'False a where + gdfrom' _ a = gdfrom $ a + gdto' _ x = gdto x + +instance (PrimCnstr fam prim a) => GDeep' fam prim 'True a where + gdfrom' _ a = Prim a + gdto' _ (Prim a) = a + +class GDeep fam prim a where + gdfrom :: a -> SFix fam prim a + gdto :: SFix fam prim a -> a + +instance GDeep' fam prim (IsElem a prim) a => GDeep fam prim a where + gdfrom = gdfrom' (Proxy :: Proxy (IsElem a prim)) + gdto = gdto' (Proxy :: Proxy (IsElem a prim)) + +dfrom :: forall fam prim a + . (CompoundCnstr fam prim a) + => a -> SFix fam prim a +dfrom = SFix + . runIdentity + . repMapCM (Proxy :: Proxy (GDeep fam prim)) + (\(I x) -> return $ gdfrom x) + . fromS + +-} + +class (CompoundCnstr kappa fam a) => Deep kappa fam a where + dfrom :: a -> SFix kappa fam a + default dfrom :: (GDeep kappa fam (Rep a)) => a -> SFix kappa fam a + dfrom = SFix . gdfrom . from + + dto :: SFix kappa fam a -> a + default dto :: (GDeep kappa fam (Rep a)) => SFix kappa fam a -> a + dto (SFix x) = to . gdto $ x + +class GDeep kappa fam f where + gdfrom :: f x -> SRep (SFix kappa fam) f + gdto :: SRep (SFix kappa fam) f -> f x + +class GDeepAtom kappa fam (isPrim :: Bool) a where + gdfromAtom :: Proxy isPrim -> a -> SFix kappa fam a + gdtoAtom :: Proxy isPrim -> SFix kappa fam a -> a + +instance (CompoundCnstr kappa fam a , Deep kappa fam a) + => GDeepAtom kappa fam 'False a where + gdfromAtom _ a = dfrom $ a + gdtoAtom _ x = dto x + +instance (PrimCnstr kappa fam a) => GDeepAtom kappa fam 'True a where + gdfromAtom _ a = Prim a + gdtoAtom _ (Prim a) = a + +instance (GDeepAtom kappa fam (IsElem a kappa) a) => GDeep kappa fam (K1 R a) where + gdfrom (K1 a) = S_K1 (gdfromAtom (Proxy :: Proxy (IsElem a kappa)) a) + gdto (S_K1 a) = K1 (gdtoAtom (Proxy :: Proxy (IsElem a kappa)) a) + +instance GDeep kappa fam U1 where + gdfrom U1 = S_U1 + gdto S_U1 = U1 + +instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :*: g) where + gdfrom (x :*: y) = (gdfrom x) :**: (gdfrom y) + gdto (x :**: y) = (gdto x) :*: (gdto y) + +instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :+: g) where + gdfrom (L1 x) = S_L1 (gdfrom x) + gdfrom (R1 x) = S_R1 (gdfrom x) + + gdto (S_L1 x) = L1 (gdto x) + gdto (S_R1 x) = R1 (gdto x) + +instance (GMeta i c , GDeep kappa fam f) => GDeep kappa fam (M1 i c f) where + gdfrom (M1 x) = S_M1 smeta (gdfrom x) + gdto (S_M1 _ x) = M1 (gdto x) diff --git a/src/Generics/Simplistic/Deep/TH.hs b/src/Generics/Simplistic/Deep/TH.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Simplistic/Deep/TH.hs @@ -0,0 +1,315 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE CPP #-} +-- |This module provides some Template Haskell functionality to +-- help out the declaration of 'Deep' instances. +-- +-- Note that we chose to not automate the whole process on purpose. +-- Sometimes the user will need to define standalone 'Generic' +-- instances for some select types in the family, some other times +-- the user might want better control over naming, for example. +-- Consequently, the most adaptable option is to provide +-- two TH utilities: +-- +-- 1. Unfolding a family into a list of types until a fixpoint is reached, +-- given in 'unfoldFamilyInto' +-- 2. Declaring 'Deep' for a list of types, given in 'declareDeepFor' +-- +-- The stepts in between unfolding the family and declaring 'Deep' vary +-- too much from case to case and hence, must be manually executed. +-- Let us run through a simple example, which involves mutual +-- recursion and type synonyms in the AST of a pseudo-language. +-- +-- > data Stmt var +-- > = SAssign var (Exp var) +-- > | SIf (Exp var) (Stmt var) (Stmt var) +-- > | SSeq (Stmt var) (Stmt var) +-- > | SReturn (Exp var) +-- > | SDecl (Decl var) +-- > | SSkip +-- > deriving (Show, Generic) +-- > +-- > data ODecl var +-- > = DVar var +-- > | DFun var var (Stmt var) +-- > deriving (Show, Generic) +-- > +-- > type Decl x = TDecl x +-- > type TDecl x = ODecl x +-- > +-- > data Exp var +-- > = EVar var +-- > | ECall var (Exp var) +-- > | EAdd (Exp var) (Exp var) +-- > | ESub (Exp var) (Exp var) +-- > | ELit Int +-- > deriving (Show, Generic) +-- +-- Now say we want to use some code written with /generics-simplistic/ +-- over these datatypes above. We must declare the 'Deep' +-- instances for the types in the family and "GHC.Generics" +-- takes care of the rest. +-- +-- The first step is in defining @Prim@ and @Fam@, which +-- will be type-level lists with the primitive types and the non-primitive, +-- or compound, types. +-- +-- An easy way to gather /all/ types involved in the family is with +-- 'unfoldFamilyInto', like: +-- +-- > unfoldFamilyInto "stmtFam" [t| Stmt Int |] +-- +-- The call above will be expanded into: +-- +-- > stmtFam :: [String] +-- > stmtFam = ["Generics.Simplistic.Example.Exp Int" +-- > ,"Generics.Simplistic.Example.ODecl Int" +-- > ,"Generics.Simplistic.Example.Stmt Int" +-- > ,"Int" +-- > ] +-- +-- Which can then be inspected with GHCi and, with +-- some elbow-grease (or test-editting macros!) we can +-- easily generate the necessary type-level lists: +-- +-- > type Fam = '[Generics.Simplistic.Example.Exp Int +-- > ,Generics.Simplistic.Example.ODecl Int +-- > ,Generics.Simplistic.Example.Stmt Int +-- > ] +-- > +-- > type Prim = '[Int] +-- +-- Finally, we are ready to call 'deriveDeepFor' and get +-- the instances declared. +-- +-- > deriveDeepFor ''Prim ''Fam +-- +-- The TH code above expands to: +-- +-- > instance Deep Prim Fam (Exp Int) +-- > instance Deep Prim Fam (ODecl Int) +-- > instance Deep Prim Fam (Stmt Int) +-- +-- This workflow is crucial to be able to work +-- with large mutually recursive families, and it becomes +-- especially easy if coupled with +-- a text editor with good macro support (read emacs and vim). +-- +module Generics.Simplistic.Deep.TH + ( unfoldFamilyInto + , deriveDeepFor + , deriveInstancesWith + ) where + +import Control.Monad.State +import Control.Arrow ((***)) + +import Language.Haskell.TH hiding (match) +import Language.Haskell.TH.Syntax hiding (lift) + +import qualified Data.Set as S + +import Generics.Simplistic.Deep + +-- |Lists all the necessary types that should +-- have 'Generic' and 'Deep' instances. For example, +-- +-- > data Rose2 a b = Fork (Either a b) [Rose2 a b] +-- > unfoldFamilyInto 'rose2tys [t| Rose2 Int Char |] +-- +-- Will yield the following code: +-- +-- > rose2tys :: String +-- > rose2tys = [ "Rose2 Int Char" +-- > , "Either Int Char" +-- > , "[Rose2 Int Char]" +-- > , "Int" +-- > , "Char" +-- > ] +-- +-- You should then use some elbow grease or your favorite text editor +-- and its provided macro functionality to produce: +-- +-- > type Rose2Prim = '[Int , Char] +-- > type Rose2Fam = '[Rose2 Int Char , Either Int Char , [Rose2 Int Char]] +-- > deriving instance Generic (Rose2 Int Char) +-- > deriving instance Generic (Either Int Char) +-- > instance Deep Rose2Prim Rose2Fam (Rose2 Int Char) +-- > instance Deep Rose2Prim Rose2Fam (Either Int Char) +-- > instance Deep Rose2Prim Rose2Fam [Rose2 Int Char] +-- +-- Note that types like @Int@ will appear fully qualified, +-- this will need some renaming. +unfoldFamilyInto :: String -> Q Type -> Q [Dec] +unfoldFamilyInto n first = do + ty <- first >>= convertType + allTys <- S.toList <$> execStateT (process ty) S.empty + listStr <- [t| [String] |] + return [ SigD (mkName n) listStr + , FunD (mkName n) [Clause [] (NormalB $ mkExp allTys) []] + ] + where + mkExp :: [STy] -> Exp + mkExp = ListE . map (LitE . StringL . show . ppr . trevnocType) + +-- |Given two type-level lists @Prims@ and @Fam@, will generate +-- @instance Deep Prim Fam f@ for every @f@ in @Fam@. +deriveDeepFor :: Name -> Name -> Q [Dec] +deriveDeepFor pr fam = + let qprim = return $ ConT pr + qfam = return $ ConT fam + in deriveInstancesWith (\t -> [t| Deep $(qprim) $(qfam) $(return t) |]) fam + +-- |Given a function @f@ and a type level stored in @fam@, +-- 'deriveInstacesWith' will generate: +-- +-- > instance f x +-- +-- for each @x@ in @fam@. This function is mostly internal, +-- please check 'deriveDeepFor' and 'deriveGenericFor'. +deriveInstancesWith :: (Type -> Q Type) -- ^ Instance to derive + -> Name -- ^ fam + -> Q [Dec] +deriveInstancesWith f fam = do + tys <- getTypeLevelList fam + forM tys $ \ty -> do + instTy <- f ty + return $ InstanceD Nothing [] instTy [] + + +getTypeLevelList :: Name -> Q [Type] +getTypeLevelList x = do + mtyDecl <- reifyDec x + case mtyDecl of + Nothing -> fail ("Not a type declaration: " ++ show (ppr x)) + Just (TySynD _ _ ty) -> getTyLL ty + Just d -> fail ("Not a type-level list: " ++ show (ppr x) ++ show (ppr d)) + where + getTyLL :: Type -> Q [Type] + getTyLL (SigT t _) = getTyLL t + getTyLL PromotedNilT = return [] + getTyLL (AppT (AppT PromotedConsT a) as) = (a:) <$> getTyLL as + getTyLL t = fail ("Not a type-level list: " ++ show (ppr x) ++ "; " ++ show t) + +process :: STy -> StateT (S.Set STy) Q () +process ty = do + tys <- get + if ty `S.member` tys + then return () + else do + let (tyHd , args) = styFlatten ty + case tyHd of + ConST tyName -> do + tyDecl <- lift (reifyDec tyName) + case tyDecl of + Just dec -> processDecl dec args + Nothing -> return () + _ -> fail "Invalid type" + +processDecl :: Dec -> [STy] -> StateT (S.Set STy) Q () +processDecl (DataD _ tyName vars _ cons _) args = do + modify (S.insert (styApp tyName args)) + let argVal = zip (map tyvarName vars) args + mapM_ (processCon argVal) cons +processDecl (NewtypeD _ tyName vars _ con _) args = do + modify (S.insert (styApp tyName args)) + let argVal = zip (map tyvarName vars) args + processCon argVal con +processDecl (TySynD _ vars ty) args = do + sty <- convertType ty + let argVal = zip (map tyvarName vars) args + process (styReduce argVal sty) +processDecl _ _ + = fail "unknown decl" + +processCon :: [(Name , STy)] -> Con -> StateT (S.Set STy) Q () +processCon argVal con = do + fields <- mapM (fmap (styReduce argVal) . convertType) (conType con) + mapM_ process fields + +tyvarName :: TyVarBndr -> Name +tyvarName (PlainTV n) = n +tyvarName (KindedTV n _) = n + +vbtyTy :: VarBangType -> Type +vbtyTy (_ , _ , t) = t + +btyTy :: BangType -> Type +btyTy (_ , t) = t + +conType :: Con -> [Type] +conType (NormalC _ btys) = map btyTy btys +conType (RecC _ vbtys) = map vbtyTy vbtys +conType (InfixC tyl _ tyr) = map btyTy [tyl , tyr] +conType (ForallC _ _ c) = conType c +conType (GadtC _ btys _) = map btyTy btys +conType (RecGadtC _ vbtys _) = map vbtyTy vbtys + +---------------------- + +data STy + = AppST STy STy + | VarST Name + | ConST Name + deriving (Eq , Show, Ord) + +#if __GLASGOW_HASKELL__ >= 808 +convertType :: (MonadFail m) => Type -> m STy +#else +convertType :: (Monad m) => Type -> m STy +#endif +convertType (AppT a b) = AppST <$> convertType a <*> convertType b +convertType (SigT t _) = convertType t +convertType (VarT n) = return (VarST n) +convertType (ConT n) = return (ConST n) +convertType (ParensT t) = convertType t +convertType ListT = return (ConST (mkName "[]")) +convertType (TupleT n) = return (ConST (mkName $ '(':replicate (n-1) ',' ++ ")")) +convertType t = fail ("convertType: Unsupported Type: " ++ show t) + +trevnocType :: STy -> Type +trevnocType (AppST a b) = AppT (trevnocType a) (trevnocType b) +trevnocType (VarST n) = VarT n +trevnocType (ConST n) + | n == mkName "[]" = ListT + | isTupleN n = TupleT $ length (show n) - 1 + | otherwise = ConT n + where isTupleN n0 = take 2 (show n0) == "(," + +-- |Handy substitution function. +-- +-- @stySubst t m n@ substitutes m for n within t, that is: t[m/n] +stySubst :: STy -> Name -> STy -> STy +stySubst (AppST a b) m n = AppST (stySubst a m n) (stySubst b m n) +stySubst (ConST a) _ _ = ConST a +stySubst (VarST x) m n + | x == m = n + | otherwise = VarST x + +-- |Just like subst, but applies a list of substitutions +styReduce :: [(Name , STy)] -> STy -> STy +styReduce parms t = foldr (\(n , m) ty -> stySubst ty n m) t parms + +-- |Flattens an application into a list of arguments; +-- +-- @styFlatten (AppST (AppST Tree A) B) == (Tree , [A , B])@ +styFlatten :: STy -> (STy , [STy]) +styFlatten (AppST a b) = id *** (++ [b]) $ styFlatten a +styFlatten sty = (sty , []) + +styApp :: Name -> [STy] -> STy +styApp name args = go (ConST name) (reverse args) + where go t [] = t + go t (x:xs) = AppST (go t xs) x + +-- * Parsing Haskell's AST + +reifyDec :: Name -> Q (Maybe Dec) +reifyDec name = + do info <- reify name + case info of TyConI dec -> return (Just dec) + _ -> return Nothing diff --git a/src/Generics/Simplistic/Derive/Eq.hs b/src/Generics/Simplistic/Derive/Eq.hs --- a/src/Generics/Simplistic/Derive/Eq.hs +++ b/src/Generics/Simplistic/Derive/Eq.hs @@ -1,23 +1,21 @@ -{-# language GADTs, - TypeFamilies, - ConstraintKinds, - TypeOperators, - FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} module Generics.Simplistic.Derive.Eq where -import Data.Functor.Identity +import Data.Proxy + import Generics.Simplistic +import Generics.Simplistic.Util -geq :: (Applicative w, OnLeaves Eq f) - => SRep w f -> SRep w f -> w Bool -geq S_U1 S_U1 = pure True -geq (S_L1 x) (S_L1 y) = geq x y -geq (S_R1 x) (S_R1 y) = geq x y -geq (x :**: y) (u :**: v) = (&&) <$> geq x u <*> geq y v -geq (S_K1 x) (S_K1 y) = (==) <$> x <*> y -geq (S_M1 _ x) (S_M1 _ y) = geq x y -geq (S_ST x) (S_ST y) = geq x y -geq _ _ = pure False +geq' :: (OnLeaves Eq f) => SRep I f -> SRep I f -> Bool +geq' x y = maybe False sameLeaves $ zipSRep x y + where + sameLeaves :: (OnLeaves Eq f) => SRep (I :*: I) f -> Bool + sameLeaves = repLeavesC (Proxy :: Proxy Eq) (uncurry' (==)) (&&) True -geq' :: (GenericSy a, OnLeaves Eq (Rep a)) => a -> a -> Bool -geq' x y = runIdentity $ geq (fromS x) (fromS y) +geq :: (Generic a, GShallow (Rep a), OnLeaves Eq (Rep a)) + => a -> a -> Bool +geq x y = geq' (fromS x) (fromS y) diff --git a/src/Generics/Simplistic/Derive/Functor.hs b/src/Generics/Simplistic/Derive/Functor.hs --- a/src/Generics/Simplistic/Derive/Functor.hs +++ b/src/Generics/Simplistic/Derive/Functor.hs @@ -1,23 +1,29 @@ -{-# language GADTs, - TypeOperators, - FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} module Generics.Simplistic.Derive.Functor where import Generics.Simplistic -gfmap :: OnLeaves1 Trivial Functor f +-- TODO: Abstract this away as a repMap1 + +-- |'SRep1' is a functor +gfmap' :: OnLeaves1 Trivial Functor f => (a -> b) -> SRep1 f a -> SRep1 f b -gfmap _ S1_U1 = S1_U1 -gfmap f (S1_L1 x) = S1_L1 (gfmap f x) -gfmap f (S1_R1 x) = S1_R1 (gfmap f x) -gfmap f (x :***: y) = gfmap f x :***: gfmap f y -gfmap f (S1_K1 x) = S1_K1 x -gfmap f (S1_M1 i x) = S1_M1 i (gfmap f x) -gfmap f (S1_ST x) = S1_ST (gfmap f x) -gfmap f (S1_Par x) = S1_Par (f x) -gfmap f (S1_Rec x) = S1_Rec (fmap f x) -gfmap f (S1_Comp x) = S1_Comp (fmap (gfmap f) x) +gfmap' _ S1_U1 = S1_U1 +gfmap' f (S1_L1 x) = S1_L1 (gfmap' f x) +gfmap' f (S1_R1 x) = S1_R1 (gfmap' f x) +gfmap' f (x :***: y) = gfmap' f x :***: gfmap' f y +gfmap' _ (S1_K1 x) = S1_K1 x +gfmap' f (S1_M1 i x) = S1_M1 i (gfmap' f x) +gfmap' f (S1_ST x) = S1_ST (gfmap' f x) +gfmap' f (S1_Par x) = S1_Par (f x) +gfmap' f (S1_Rec x) = S1_Rec (fmap f x) +gfmap' f (S1_Comp x) = S1_Comp (fmap (gfmap' f) x) -gfmap' :: (GenericSy1 f, OnLeaves1 Trivial Functor (Rep1 f)) - => (a -> b) -> f a -> f b -gfmap' f x = toS1 $ gfmap f $ fromS1 x +-- |The action of f over arrows can be obtained by translating +-- into the generic representation, using the generic +-- 'gfmap'' and translating back to regular representation. +gfmap :: (Simplistic1 f, OnLeaves1 Trivial Functor (Rep1 f)) + => (a -> b) -> f a -> f b +gfmap f = toS1 . gfmap' f . fromS1 diff --git a/src/Generics/Simplistic/Derive/Show.hs b/src/Generics/Simplistic/Derive/Show.hs --- a/src/Generics/Simplistic/Derive/Show.hs +++ b/src/Generics/Simplistic/Derive/Show.hs @@ -1,43 +1,42 @@ -{-# language GADTs, - TypeFamilies, - ConstraintKinds, - TypeOperators, - FlexibleContexts, - ScopedTypeVariables, - DeriveGeneric #-} -module Generics.Simplistic.Derive.Show where +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveGeneric #-} +-- |Derives a generic show, for example +-- +-- > data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic +-- > +-- > myListValue :: MyList Integer +-- > myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil)) +-- > +-- > instance Show a => Show (MyList a) where +-- > show = gshow +-- +-- The code here was adapted from `generic-deriving` +-- https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs +module Generics.Simplistic.Derive.Show (gshow , gshowsPrec) where -import Data.Functor.Identity import Generics.Simplistic import GHC.Generics --- An example -data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic - -myListValue :: MyList Integer -myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil)) - -instance Show a => Show (MyList a) where - show = gshow - --- Translated from `generic-deriving` --- https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs - appPrec :: Int appPrec = 2 data Type = Rec | Tup | Pref | Inf String -gshow :: (GenericSy t, OnLeaves Show (Rep t)) +gshow :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t)) => t -> String gshow v = gshowsPrec Pref 0 v "" -gshowsPrec :: (GenericSy t, OnLeaves Show (Rep t)) +gshowsPrec :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t)) => Type -> Int -> t -> ShowS gshowsPrec t n v = gshowsPrec' t n (fromS v) gshowsPrec' :: (OnLeaves Show f) - => Type -> Int -> SRep Identity f -> ShowS + => Type -> Int -> SRep I f -> ShowS -- "Simple" cases gshowsPrec' _ _ S_U1 = id gshowsPrec' t n (S_L1 x) = gshowsPrec' t n x @@ -54,7 +53,7 @@ gshowsPrec' t@Pref n (a :**: b) = gshowsPrec' t (n+1) a . showChar ' ' . gshowsPrec' t (n+1) b -- The case of metadata -gshowsPrec' t n (S_M1 (SM_C :: SMeta i c) (x :: SRep Identity f)) = +gshowsPrec' _ n (S_M1 (SM_C :: SMeta i c) (x :: SRep I f)) = case fixity of Prefix -> showParen (n > appPrec && not (isNullary x)) ( showString (conName c) @@ -78,7 +77,7 @@ conIsTuple y = tupleName (conName y) where tupleName ('(':',':_) = True tupleName _ = False -gshowsPrec' t n (S_M1 (SM_S :: SMeta i c) (x :: SRep Identity f)) +gshowsPrec' t n (S_M1 (SM_S :: SMeta i c) (x :: SRep I f)) | selName s == "" = --showParen (n > appPrec) (gshowsPrec' t n x) | otherwise = showString (selName s) @@ -87,12 +86,12 @@ where s :: M1 S c f () = undefined gshowsPrec' t n (S_M1 _ x) = gshowsPrec' t n x -isNullary :: SRep Identity a -> Bool +isNullary :: SRep I a -> Bool isNullary S_U1 = True -isNullary (S_L1 x) = error "unnecessary case" -isNullary (S_R1 x) = error "unnecessary case" -isNullary (x :**: y) = False -isNullary (S_K1 x) = False +isNullary (S_L1 _) = error "unnecessary case" +isNullary (S_R1 _) = error "unnecessary case" +isNullary (_ :**: _) = False +isNullary (S_K1 _) = False isNullary (S_M1 t x) = case t of SM_S -> isNullary x _ -> error "unnecessary case" diff --git a/src/Generics/Simplistic/Unify.hs b/src/Generics/Simplistic/Unify.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Simplistic/Unify.hs @@ -0,0 +1,289 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- |Constraint-based unification algorithm for 'Holes' +module Generics.Simplistic.Unify + ( -- * Substitution + Subst , substEmpty , substInsert , substLkup , substApply + -- * Unification + , UnifyErr(..) , unify , unify_ , unifyWith , minimize + ) where + +import Data.List (sort) +import qualified Data.Map as M +import Control.Monad.Except +import Control.Monad.State +import Control.Monad.Writer hiding (All) +import Control.Monad.Cont +import Unsafe.Coerce + +import Generics.Simplistic.Deep +import Generics.Simplistic.Util + +-- |Unification can return succesfully or find either +-- a 'OccursCheck' failure or a 'SymbolClash' failure. +data UnifyErr kappa fam phi :: * where + -- |The occurs-check fails when the variable in question + -- occurs within the term its supposed to be unified with. + OccursCheck :: [Exists phi] + -> UnifyErr kappa fam phi + -- |A symbol-clash is thrown when the head of the + -- two terms is different and neither is a variabe. + SymbolClash :: Holes kappa fam phi at + -> Holes kappa fam phi at + -> UnifyErr kappa fam phi + +-- |A substitution is but a map; the existential quantifiers are +-- necessary to ensure we can reuse from "Data.Map" +-- +-- Note that we must be able to compare @Exists phi@. This +-- comparison needs to work heterogeneously and it must +-- return 'EQ' only when the contents are in fact equal. +-- Even though we only need this instance for "Data.Map" +-- +-- A typical example for @phi@ is @Const Int at@, representing +-- a variable. The @Ord@ instance would then be: +-- +-- > instance Ord (Exists (Const Int)) where +-- > compare (Exists (Const x)) (Exists (Const y)) +-- > = compare x y +-- +type Subst kappa fam phi + = M.Map (Exists phi) (Exists (Holes kappa fam phi)) + +-- |Empty substitution +substEmpty :: Subst kappa fam phi +substEmpty = M.empty + +-- |Looks a value up in a substitution, see 'substInsert' +substLkup :: (Ord (Exists phi)) + => Subst kappa fam phi -- ^ + -> phi at + -> Maybe (Holes kappa fam phi at) +substLkup sigma var = + case M.lookup (Exists var) sigma of + Nothing -> Nothing + -- In case we found something, it must be of the same + -- type as what we got because we only insert + -- well-typed things. + -- TODO: Use our sameTy method to remove the unsafeCoerce + Just (Exists t) -> Just $ unsafeCoerce t + +-- |Applies a substitution to a term once; Variables not in the +-- support of the substitution are left untouched. +substApply :: (Ord (Exists phi)) + => Subst kappa fam phi -- ^ + -> Holes kappa fam phi at + -> Holes kappa fam phi at +substApply sigma = holesJoin + . holesMap (\v -> maybe (Hole v) id $ substLkup sigma v) + +-- |Inserts a point in a substitution. Note how the index of +-- @phi@ /must/ match the index of the term being inserted. +-- This is important when looking up terms because we must +-- 'unsafeCoerce' the existential type variables to return. +-- +-- Please, always use this insertion function; or, if you insert +-- by hand, ensure thetype indices match. +substInsert :: (Ord (Exists phi)) + => Subst kappa fam phi -- ^ + -> phi at + -> Holes kappa fam phi at + -> Subst kappa fam phi +substInsert sigma v x = M.insert (Exists v) (Exists x) sigma + +-- |Unification is done in a monad. +type UnifyM kappa fam phi + = StateT (Subst kappa fam phi) (Except (UnifyErr kappa fam phi)) + +-- |Attempts to unify two 'Holes', but ignores +-- which error happened when they could not be unified. +unify_ :: (All Eq kappa , Ord (Exists phi) , EqHO phi) + => Holes kappa fam phi at -- ^ + -> Holes kappa fam phi at + -> Maybe (Subst kappa fam phi) +unify_ a = either (const Nothing) Just + . runExcept . unify a + +-- |Attempts to unify two 'Holes' +unify :: (All Eq kappa , Ord (Exists phi) , EqHO phi) + => Holes kappa fam phi at -- ^ + -> Holes kappa fam phi at + -> Except (UnifyErr kappa fam phi) + (Subst kappa fam phi) +unify = unifyWith substEmpty + +-- |Attempts to unify two 'Holes' with an already existing +-- substitution +unifyWith :: (All Eq kappa , Ord (Exists phi) , EqHO phi) + => Subst kappa fam phi -- ^ Starting subst + -> Holes kappa fam phi at + -> Holes kappa fam phi at + -> Except (UnifyErr kappa fam phi) + (Subst kappa fam phi) +unifyWith sigma x y = execStateT (unifyM x y) sigma + +-- Actual unification algorithm; In order to improve efficiency, +-- we first register all equivalences we need to satisfy, +-- then on 'mininize' we do the occurs-check. +unifyM :: forall kappa fam phi at + . (All Eq kappa , EqHO phi , Ord (Exists phi)) + => Holes kappa fam phi at + -> Holes kappa fam phi at + -> UnifyM kappa fam phi () +unifyM x y = do + _ <- getEquivs x y + s <- get + case minimize s of + Left vs -> throwError (OccursCheck vs) + Right s' -> put s' + where + getEquivs :: Holes kappa fam phi b + -> Holes kappa fam phi b + -> UnifyM kappa fam phi () + getEquivs p q = void $ holesMapM (uncurry' getEq) (lgg p q) + + getEq :: Holes kappa fam phi b + -> Holes kappa fam phi b + -> UnifyM kappa fam phi (Holes kappa fam phi b) + getEq p (Hole var) = record_eq var p >> return p + getEq p@(Hole var) q = record_eq var q >> return p + getEq p q | eqHO p q = return p + | otherwise = throwError (SymbolClash p q) + + -- Whenever we see a variable being matched against a term + -- we record the equivalence. First we make sure we did not + -- record such equivalence yet, otherwise, we recursively thin + record_eq :: phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi () + record_eq var q = do + sigma <- get + case substLkup sigma var of + -- First time we see 'var', we instantiate it and get going. + Nothing -> when (not $ eqHO q (Hole var)) + $ modify (\s -> substInsert s var q) + -- It's not the first time we thin 'var'; previously, we had + -- that 'var' was supposed to be p'. We will check whether it + -- is the same as q, if not, we will have to thin p' with q. + Just q' -> unless (eqHO q' q) + $ void $ getEquivs q q' + + +-- |The minimization step performs the /occurs check/ and removes +-- unecessary steps, returning an idempodent substitution when +-- successful. For example; +-- +-- > sigma = fromList +-- > [ (0 , bin 1 2) +-- > , (1 , bin 4 4) ] +-- +-- Then, @minimize sigma@ will return @fromList [(0 , bin (bin 4 4) 2) , (1 , bin 4 4)]@ +-- This returns @Left vs@ if occurs-check fail for variables @vs@. +-- +minimize :: forall kappa fam phi . (Ord (Exists phi)) + => Subst kappa fam phi -- ^ + -> Either [Exists phi] (Subst kappa fam phi) +minimize sigma = + let sigma' = breakCycles inj proj $ removeIds proj sigma + in whileM sigma' [] $ \s _ + -> M.fromList <$> (mapM (secondF (exMapM (go sigma'))) (M.toList s)) + where + inj :: Exists phi -> Exists (Holes kappa fam phi) + inj = exMap Hole + + proj :: Exists (Holes kappa fam phi) -> Maybe (Exists phi) + proj (Exists (Hole phi)) = Just $ Exists phi + proj _ = Nothing + + secondF :: (Functor m) => (a -> m b) -> (x , a) -> m (x , b) + secondF f (x , a) = (x,) <$> f a + + -- The actual engine of the 'minimize' function is thinning the + -- variables that appear in the image of the substitution under production. + -- We use the writer monad solely to let us know whether some variables have + -- been substituted in this current term. After one iteration + -- of the map where no variable is further refined, we are done. + go :: Subst kappa fam phi + -> Holes kappa fam phi at + -> Writer [Exists phi] (Holes kappa fam phi at) + go ss = holesRefineHolesM $ \var -> do + case substLkup ss var of + Nothing -> return (Hole var) + Just r -> tell [Exists var] + >> return r + + -- | Just like nub; but works on a sorted list + mnub :: (Ord a) => [a] -> [a] + mnub [] = [] + mnub [x] = [x] + mnub (x:y:ys) + | x == y = mnub (y:ys) + | otherwise = x : mnub (y:ys) + + -- We loop while there is work to be done or no progress + -- was done. + whileM :: (Ord (Exists phi)) + => a -> [Exists phi] -> (a -> [Exists phi] -> Writer [Exists phi] a) + -> Either [Exists phi] a + whileM a xs f = do + let (x' , xs') = runWriter (f a xs) + if null xs' + then return x' + else if (mnub (sort xs') == mnub (sort xs)) + then Left xs' + else whileM x' xs' f + +-- |Removes the keys that project to themselves according to +-- the provided projection. +-- +-- > removeIds id $ M.fromList [(0,0), (1,2) , (3,4)] +-- > = M.fromList [(1,2),(3,4)] +-- +removeIds :: forall a b + . (Ord a) => (b -> Maybe a) -> M.Map a b -> M.Map a b +removeIds proj = M.filterWithKey (\a b -> not $ Just a == proj b) + + +-- |Will make sure there are no cycles in the map as per the +-- provided function. For example, +-- +-- > breakCycles id Just $ M.fromList [(0,1) , (1,2) , (2,0)] +-- > = M.fromList [(1,0),(2,0)] +-- +-- Usefull when the maps represent some sort of equivalence; the function +-- essentially collapses the equivalence class. +breakCycles :: forall a b + . (Ord a) => (a -> b) -> (b -> Maybe a) -> M.Map a b -> M.Map a b +breakCycles inj proj m0 + = let (flattenedCycles , m') = runState (dropCycles m0) M.empty + in M.union flattenedCycles m' + where + dropCycles :: M.Map a b -> State (M.Map a b) (M.Map a b) + dropCycles m = case findCycle m of + Nothing -> return m + Just (a , cyc) -> do + modify (M.union cyc) + dropCycles (M.delete a (m M.\\ cyc)) + + cycleFor :: a -> M.Map a b -> Maybe (M.Map a b) + cycleFor a0 m = M.lookup a0 m >>= proj >>= go M.empty + where + go :: M.Map a b -> a -> Maybe (M.Map a b) + go aux a' + | a' == a0 || a' `M.member` aux = return aux + | otherwise = M.lookup a' m >>= proj >>= go (M.insert a' (inj a0) aux) + + findCycle :: M.Map a b -> Maybe (a , M.Map a b) + findCycle m = (`runCont` id) $ callCC $ + \exit -> (>> return Nothing) . flip mapM_ (M.keys m) $ + \a -> case cycleFor a m of + Nothing -> return () + Just r -> exit $ Just (a , r) diff --git a/src/Generics/Simplistic/Util.hs b/src/Generics/Simplistic/Util.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Simplistic/Util.hs @@ -0,0 +1,249 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE PatternSynonyms #-} +module Generics.Simplistic.Util + ( -- * Utility Functions and Types + (&&&) , (***) , (:->) , (<.>) + -- * Poly-kind indexed product functionality + , (:*:)(..) , Delta , curry' , uncurry' , delta , deltaMap + -- * Poly-kind indexed sums + , Sum(..) , either' , either'' + -- * Constraints + , Implies , Trivial + -- * Higher-order Eq and Show + , EqHO(..) , ShowHO(..) + -- * Existential Wrapper + , Exists(..) , exMap , exMapM , exElim + -- * Elem functionality + , Elem , NotElem , HasElem(..) , ElemPrf(..) , IsElem, sameTy + -- * Witnessing and All constraints + , All , Witness(..) , witness , witnessPrf + , weq , wshow + ) where + +import Data.Kind (Constraint) +import Data.Proxy (Proxy(..)) +import Data.Functor.Sum +import Data.Functor.Const +import Data.Type.Equality +import Control.Arrow ((***) , (&&&)) +import GHC.Generics ((:*:)(..), V1 , U1(..)) + +-- |Lifted curry +curry' :: ((f :*: g) x -> a) -> f x -> g x -> a +curry' f fx gx = f (fx :*: gx) + +-- |Lifted uncurry +uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a +uncurry' f (fx :*: gx) = f fx gx + +-- |Natural transformations +type f :-> g = forall n . f n -> g n + +-- |Diagonal indexed functor +type Delta f = f :*: f + +-- |Duplicates its argument +delta :: f :-> Delta f +delta fx = fx :*: fx + +-- |Applies the same function to both components of the pair +deltaMap :: (f :-> g) -> Delta f :-> Delta g +deltaMap f (x :*: y) = f x :*: f y + +-- |Higher-order sum eliminator +either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r +either' f _ (InL x) = f x +either' _ g (InR x) = g x + +-- |Just like 'either'', but the result type is of kind Star +either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a +either'' f g = getConst . either' (Const . f) (Const . g) + +infixr 8 <.> +-- |Kleisli Composition +(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c +f <.> g = (>>= f) . g + +-- |Constraint implication +class (c => d) => Implies c d +instance (c => d) => Implies c d + +-- |Trivial constraint +class Trivial c +instance Trivial c + +-- |Higher order , poly kinded, version of 'Eq' +class EqHO (f :: ki -> *) where + eqHO :: forall k . f k -> f k -> Bool + +instance Eq a => EqHO (Const a) where + eqHO (Const a) (Const b) = a == b + +instance (EqHO f, EqHO g) => EqHO (f :*: g) where + eqHO (fx :*: gx) (fy :*: gy) = eqHO fx fy && eqHO gx gy + +instance (EqHO f, EqHO g) => EqHO (Sum f g) where + eqHO (InL fx) (InL fy) = eqHO fx fy + eqHO (InR gx) (InR gy) = eqHO gx gy + eqHO _ _ = False + +instance EqHO V1 where + eqHO _ _ = True + +instance EqHO U1 where + eqHO _ _ = True + + + +-- |Higher order, poly kinded, version of 'Show'; We provide +-- the same 'showsPrec' mechanism. The documentation of "Text.Show" +-- has a good example of the correct usage of 'showsPrec': +-- +-- > +-- > infixr 5 :^: +-- > data Tree a = Leaf a | Tree a :^: Tree a +-- > +-- > instance (Show a) => Show (Tree a) where +-- > showsPrec d (Leaf m) = showParen (d > app_prec) $ +-- > showString "Leaf " . showsPrec (app_prec+1) m +-- > where app_prec = 10 +-- > +-- > showsPrec d (u :^: v) = showParen (d > up_prec) $ +-- > showsPrec (up_prec+1) u . +-- > showString " :^: " . +-- > showsPrec (up_prec+1) v +-- > where up_prec = 5 +-- +class ShowHO (f :: ki -> *) where + showHO :: forall k . f k -> String + showsPrecHO :: forall k . Int -> f k -> ShowS + {-# MINIMAL showHO | showsPrecHO #-} + + showHO fx = showsPrecHO 0 fx "" + showsPrecHO _ fx s = showHO fx ++ s + +instance Show a => ShowHO (Const a) where + showsPrecHO d (Const a) = showParen (d > app_prec) $ + showString "Const " . showsPrec (app_prec + 1) a + where app_prec = 10 + +instance (ShowHO f , ShowHO g) => ShowHO (f :*: g) where + showsPrecHO d (x :*: y) = showParen (d > app_prec) $ + showsPrecHO (app_prec+1) x + . showString " :*: " + . showsPrecHO (app_prec+1) y + where app_prec = 10 + +instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where + showsPrecHO d (InL fx) = showParen (d > app_prec) $ + showString "InL " . showsPrecHO (app_prec + 1) fx + where app_prec = 10 + showsPrecHO d (InR gx) = showParen (d > app_prec) $ + showString "InR " . showsPrecHO (app_prec + 1) gx + where app_prec = 10 + +-- |Existential type wrapper. This comesin particularly +-- handy when we want to add mrsop terms to +-- some container. See "Generics.MRSOP.Holes.Unify" for example. +data Exists (f :: k -> *) :: * where + Exists :: f x -> Exists f + +-- |Maps over 'Exists' +exMap :: (forall x . f x -> g x) -> Exists f -> Exists g +exMap f (Exists x) = Exists (f x) + +-- |Maps a monadic actino over 'Exists' +exMapM :: (Monad m) => (forall x . f x -> m (g x)) -> Exists f -> m (Exists g) +exMapM f (Exists x) = Exists <$> f x + +-- |eliminates an 'Exists' +exElim :: (forall x . f x -> a) -> Exists f -> a +exElim f (Exists x) = f x + +instance ShowHO f => Show (Exists f) where + show = exElim showHO + +-- Boolean predicate about being element of a list +type family IsElem (a :: k) (as :: [ k ]) :: Bool where + IsElem a (a ': as) = 'True + IsElem a (b ': as) = IsElem a as + IsElem a '[] = 'False + +-- An actual proof that something is an element +data ElemPrf a as where + Here :: ElemPrf a (a ': as) + There :: ElemPrf a as -> ElemPrf a (b ': as) + +-- Constructing these proofs +class HasElem a as where + hasElem :: ElemPrf a as +instance {-# OVERLAPPING #-} HasElem a (a ': as) where + hasElem = Here +instance {-# OVERLAPPABLE #-} + (HasElem a as) => HasElem a (b ': as) where + hasElem = There hasElem + +-- |We will carry constructive information on the +-- constraint. Forcing 'IsElem' to true +type Elem a as = (IsElem a as ~ 'True , HasElem a as) + +-- |Negation of 'Elem' +type NotElem a as = IsElem a as ~ 'False + +-- |Returns whether two types are the same, given that +-- both belong to the same list. +sameTy :: forall fam x y . (Elem x fam , Elem y fam) + => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y) +sameTy _ _ _ = go (hasElem :: ElemPrf x fam) (hasElem :: ElemPrf y fam) + where + go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b) + go Here Here = Just Refl + go (There rr) (There y) = go rr y + go _ _ = Nothing + +type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where + All c '[] = () + All c (x ': xs) = (c x , All c xs) + +-- |Carries information about @x@ being an instance of @c@ +data Witness c x where + Witness :: (c x) => Witness c x + +-- |Provides the witness that @x@ is an instance of @c@ +witness :: forall x xs c + . (HasElem x xs , All c xs) + => Proxy xs -> Witness c x +witness _ = witnessPrf (hasElem :: ElemPrf x xs) + +-- |Fetches the 'Eq' instance for an element of a list +weq :: forall x xs + . (All Eq xs , Elem x xs) + => Proxy xs -> x -> x -> Bool +weq p = case witness p :: Witness Eq x of + Witness -> (==) + +-- |Fetches the 'Eq' instance for an element of a list +wshow :: forall x xs + . (All Show xs , Elem x xs) + => Proxy xs -> x -> String +wshow p = case witness p :: Witness Show x of + Witness -> show + +-- |Provides the witness that @x@ is an instance of @c@ +witnessPrf :: (All c xs) => ElemPrf x xs -> Witness c x +witnessPrf Here = Witness +witnessPrf (There p) = witnessPrf p + diff --git a/src/Generics/Simplistic/Zipper.hs b/src/Generics/Simplistic/Zipper.hs new file mode 100644 --- /dev/null +++ b/src/Generics/Simplistic/Zipper.hs @@ -0,0 +1,173 @@ +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- |Provides bare-bones /zipper/ functionality +-- to 'SRep' and 'Holes'. +module Generics.Simplistic.Zipper where + +import Data.Proxy +import Data.Type.Equality +import GHC.Generics +import Data.Functor.Sum +import Control.Arrow (first) + +import Generics.Simplistic +import Generics.Simplistic.Deep +import Generics.Simplistic.Util + +-- |A value of type 'SZip ty w f' corresponds to a value of type +-- 'SRep w f' with one of its leaves of type @w ty@ absent. +-- This is essentially a zipper for 'SRep'. +data SZip ty w f where + Z_KH :: SZip ty w (K1 i ty) + + Z_L1 :: SZip ty w f -> SZip ty w (f :+: g) + Z_R1 :: SZip ty w g -> SZip ty w (f :+: g) + Z_PairL :: SZip ty w f -> SRep w g -> SZip ty w (f :*: g) + Z_PairR :: SRep w f -> SZip ty w g -> SZip ty w (f :*: g) + Z_M1 :: SMeta i t -> SZip ty w f -> SZip ty w (M1 i t f) +deriving instance (forall a. Show (w a)) => Show (SZip h w f) +deriving instance (forall a. Eq (w a)) => Eq (SZip h w f) + +-- |We can transform a 'SZip' into a 'SRep' given +-- we are provided with a value to /plug/ into the identified position. +plug :: SZip ty phi f -> phi ty -> SRep phi f +plug Z_KH k = S_K1 k +plug (Z_L1 x) k = S_L1 $ plug x k +plug (Z_R1 x) k = S_R1 $ plug x k +plug (Z_M1 c x) k = S_M1 c $ plug x k +plug (Z_PairL x y) k = (plug x k) :**: y +plug (Z_PairR x y) k = x :**: (plug y k) + +-- |Maps over a 'SZip' +zipperMap :: (forall x . h x -> g x) + -> SZip ty h f -> SZip ty g f +zipperMap f (Z_L1 x) = Z_L1 (zipperMap f x) +zipperMap f (Z_R1 x) = Z_R1 (zipperMap f x) +zipperMap f (Z_M1 c x) = Z_M1 c (zipperMap f x) +zipperMap f (Z_PairL x y) = Z_PairL (zipperMap f x) (repMap f y) +zipperMap f (Z_PairR x y) = Z_PairR (repMap f x) (zipperMap f y) +zipperMap _ Z_KH = Z_KH + +inr1 :: (x :*: y) t -> (Sum z x :*: y) t +inr1 (x :*: y) = (InR x :*: y) + +-- |Given a @z :: SZip ty h f@ and a @r :: Rep w f@, if @z@ and @r@ +-- are made with the same constuctor we return a representation +-- that contains both @h@s and @w@s in its leaves, except in one leaf +-- of type @ty@. This is analogous to 'zipSRep'. +zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep ((Sum ((:~:) ty) h) :*: w) f) +zipperRepZip Z_KH (S_K1 y) = return $ S_K1 (InL Refl :*: y) +zipperRepZip (Z_L1 x) (S_L1 y) = S_L1 <$> zipperRepZip x y +zipperRepZip (Z_R1 x) (S_R1 y) = S_R1 <$> zipperRepZip x y +zipperRepZip (Z_M1 c x) (S_M1 _ y) = S_M1 c <$> zipperRepZip x y +zipperRepZip (Z_PairL x y) (y1 :**: y2) + = (:**:) <$> zipperRepZip x y1 <*> (repMap inr1 <$> zipSRep y y2) +zipperRepZip (Z_PairR x y) (y1 :**: y2) + = (:**:) <$> (repMap inr1 <$> zipSRep x y1) <*> zipperRepZip y y2 +zipperRepZip _ _ = Nothing + +-- |Overlaps two zippers together; only succeeds if both zippers +-- have the same constructor AND hole. +zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f) +zipSZip Z_KH Z_KH = Just Z_KH +zipSZip (Z_L1 x) (Z_L1 y) = Z_L1 <$> zipSZip x y +zipSZip (Z_R1 x) (Z_R1 y) = Z_R1 <$> zipSZip x y +zipSZip (Z_M1 c x) (Z_M1 _ y) = Z_M1 c <$> zipSZip x y +zipSZip (Z_PairL x y) (Z_PairL w z) + = Z_PairL <$> zipSZip x w <*> zipSRep y z +zipSZip (Z_PairR x y) (Z_PairR w z) + = Z_PairR <$> zipSRep x w <*> zipSZip y z +zipSZip _ _ = Nothing + +-- |Analogous to 'repLeavesList' +zipLeavesList :: SZip ty w f -> [Maybe (Exists w)] +zipLeavesList (Z_L1 x) = zipLeavesList x +zipLeavesList (Z_R1 x) = zipLeavesList x +zipLeavesList (Z_M1 _ x) = zipLeavesList x +zipLeavesList (Z_PairL l x) = zipLeavesList l ++ map Just (repLeavesList x) +zipLeavesList (Z_PairR x l) = map Just (repLeavesList x) ++ zipLeavesList l +zipLeavesList (Z_KH ) = [Nothing] + +-- |The 'Zipper' datatype packages a 'SZip' in a more standard +-- presentation. A value of type @Zipper c f g t@ represents +-- a value of type @SRep f t@, where exactly one recursive leaf (of type @t@) +-- carries a value of type @g t@, moreover, we also carry a proof that +-- the constraint @c@ holds. +data Zipper c f g t where + Zipper :: c + => { zipper :: SZip t f (Rep t) + , sel :: g t + } + -> Zipper c f g t + +-- |Auxiliar type synonym for annotated fixpoints. +type Zipper' kappa fam ann phi t + = Zipper (CompoundCnstr kappa fam t) + (HolesAnn kappa fam ann phi) + (HolesAnn kappa fam ann phi) t + +-- |Given a function that checks wheter an arbitrary position +-- is recursive and a value of @t@, returns all possible zippers ove +-- @t@. +zippers :: forall kappa fam ann phi t + . (forall a . (Elem t fam) => phi a -> Maybe (a :~: t)) + -> HolesAnn kappa fam ann phi t + -> [Zipper' kappa fam ann phi t] +zippers _ (Prim' _ _) = [] +zippers _ (Hole' _ _) = [] +zippers aux (Roll' _ r) = map (uncurry Zipper) (go r) + where + pf :: Proxy fam + pf = Proxy + + pa :: HolesAnn kappa fam ann phi a -> Proxy a + pa _ = Proxy + + go :: SRep (HolesAnn kappa fam ann phi) f + -> [(SZip t (HolesAnn kappa fam ann phi) f + , HolesAnn kappa fam ann phi t)] + go S_U1 = [] + go (S_L1 x) = first Z_L1 <$> go x + go (S_R1 x) = first Z_R1 <$> go x + go (S_M1 c x) = first (Z_M1 c) <$> go x + go (x :**: y) = (first (flip Z_PairL y) <$> go x) + ++ (first (Z_PairR x) <$> go y) + go (S_K1 x@(Roll' _ _)) = + case sameTy pf (Proxy :: Proxy t) (pa x) of + Just Refl -> return $ (Z_KH , x) + Nothing -> [] + go (S_K1 x@(Hole' _ xh)) = + case aux xh of + Just Refl -> return $ (Z_KH , x) + Nothing -> [] + go _ = [] + +-- |Retrieves the constructor name for a representation. +-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of +-- a type constructed with "GHC.Generics" builtin mechanisms. +zipConstructorName :: SZip h w f -> String +zipConstructorName (Z_M1 x@SM_C _) + = getConstructorName x +zipConstructorName (Z_M1 _ x) + = zipConstructorName x +zipConstructorName (Z_L1 x) + = zipConstructorName x +zipConstructorName (Z_R1 x) + = zipConstructorName x +zipConstructorName _ + = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep" +