From abfd8b492a7c2c652bf011cb6bb09746793bb27d Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 14 Jul 2023 12:20:49 +0200 Subject: [PATCH 01/54] add cabal-docspec to flake dependencies Currently from the Nix user repo because it is not yet on hackage or nixpkgs --- flake.lock | 18 +++++++++++++++++- flake.nix | 9 +++++++-- 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/flake.lock b/flake.lock index c566578..fbae18a 100644 --- a/flake.lock +++ b/flake.lock @@ -31,10 +31,26 @@ "type": "github" } }, + "nur": { + "locked": { + "lastModified": 1689328451, + "narHash": "sha256-WWJXUi3mT05cNBQ9YwLO/AqWyaTOxmHEp7EdJlkioM4=", + "owner": "nix-community", + "repo": "nur", + "rev": "1839d2b991671f63666cdb0716875a2dd8ba4a46", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nur", + "type": "github" + } + }, "root": { "inputs": { "flake-utils": "flake-utils", - "nixpkgs": "nixpkgs" + "nixpkgs": "nixpkgs", + "nur": "nur" } } }, diff --git a/flake.nix b/flake.nix index 8c47fc7..419b5f9 100644 --- a/flake.nix +++ b/flake.nix @@ -3,12 +3,16 @@ inputs = { nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable"; + nur.url = "github:nix-community/nur"; flake-utils.url = "github:numtide/flake-utils"; }; - outputs = { self, nixpkgs, flake-utils }: + outputs = { self, nixpkgs, nur, flake-utils }: flake-utils.lib.eachDefaultSystem (system: let - + nurpkgs = import nur { + nurpkgs = nixpkgs.legacyPackages.x86_64-linux; + pkgs = nixpkgs.legacyPackages.x86_64-linux; + }; compiler = "8107"; # compiler = "921"; pkgs = import nixpkgs { @@ -52,6 +56,7 @@ buildInputs = [ ghc hspkgs.cabal-install + nurpkgs.repos.amesgen.cabal-docspec ]; }; }); From bd88680c9eb4fb12a828cde09e04b382f26b749c Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 15 Jul 2023 10:17:56 +0200 Subject: [PATCH 02/54] fix CoRec test for match --- Data/Vinyl/CoRec.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/CoRec.hs b/Data/Vinyl/CoRec.hs index 6a47b15..ce85ad4 100644 --- a/Data/Vinyl/CoRec.hs +++ b/Data/Vinyl/CoRec.hs @@ -202,8 +202,12 @@ asA' f@(CoRec x) -- | Pattern match on a CoRec by specifying handlers for each case. Note that -- the order of the Handlers has to match the type level list (t:ts). -- +-- >>> :set -XDataKinds +-- >>> import Data.Vinyl.Core ( Rec((:&), RNil)) +-- >>> import Data.Vinyl.Functor (Identity(Identity)) +-- >>> import Data.Vinyl.CoRec (CoRec(CoRec), match, Handler(H)) -- >>> :{ --- let testCoRec = Col (Identity False) :: CoRec Identity [Int, String, Bool] in +-- let testCoRec = CoRec (Identity False) :: CoRec Identity [Int, String, Bool] in -- match testCoRec $ -- (H $ \i -> "my Int is the successor of " ++ show (i - 1)) -- :& (H $ \s -> "my String is: " ++ s) From c61336b078371e82f32da7ce97ff0de79fce58c2 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 15 Jul 2023 11:37:55 +0200 Subject: [PATCH 03/54] fix Curry doctests --- Data/Vinyl/Curry.hs | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Curry.hs b/Data/Vinyl/Curry.hs index e61026b..f34f4df 100644 --- a/Data/Vinyl/Curry.hs +++ b/Data/Vinyl/Curry.hs @@ -123,9 +123,9 @@ runcurryX f = xruncurry f . toXRec {-| Lift an N-ary function to work over a record of 'Applicative' computations. +>>> import Data.Vinyl.Core ( Rec((:&), RNil) ) >>> runcurryA' (+) (Just 2 :& Just 3 :& RNil) Just 5 - >>> runcurryA' (+) (Nothing :& Just 3 :& RNil) Nothing -} @@ -179,9 +179,17 @@ For the type-level list @ts@, @'CurriedX' f ts a@ is a curried function type from arguments of type @HKD f t@ for @t@ in @ts@, to a result of type @a@. >>> :set -XTypeOperators +>>> import Data.Vinyl.Functor ((:.), Identity(Identity)) +>>> import Data.Vinyl.Curry (CurriedX) >>> :kind! CurriedX (Maybe :. Identity) '[Int, Bool, String] Int CurriedX (Maybe :. Identity) '[Int, Bool, String] Int :: * -= Maybe Int -> Maybe Bool -> Maybe [Char] -> Int += Data.Vinyl.XRec.HKD + (Data.Vinyl.Functor.Compose Maybe Identity) Int + -> Data.Vinyl.XRec.HKD + (Data.Vinyl.Functor.Compose Maybe Identity) Bool + -> Data.Vinyl.XRec.HKD + (Data.Vinyl.Functor.Compose Maybe Identity) [Char] + -> Int -} type family CurriedX (f :: u -> Type) (ts :: [u]) a where CurriedX f '[] a = a From 16d8f2e1e254761490ad7d5747c7a391fb87da4a Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 15 Jul 2023 11:33:23 +0200 Subject: [PATCH 04/54] fix Tutorial doctest Unfortunately this requires introducing singletons as dependencies. I don't know how to best solve this. --- Data/Vinyl/Tutorial/Overview.hs | 4 +++- vinyl.cabal | 7 ++++++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Tutorial/Overview.hs b/Data/Vinyl/Tutorial/Overview.hs index c17e7ef..568b7c7 100644 --- a/Data/Vinyl/Tutorial/Overview.hs +++ b/Data/Vinyl/Tutorial/Overview.hs @@ -7,6 +7,7 @@ Let's work through a quick example. We'll need to enable some language extensions first: +>>> :set -package lens >>> :set -XDataKinds >>> :set -XPolyKinds @@ -15,6 +16,7 @@ >>> :set -XTypeFamilies >>> :set -XFlexibleContexts >>> :set -XFlexibleInstances +>>> :set -XStandaloneKindSignatures >>> :set -XNoMonomorphismRestriction >>> :set -XGADTs >>> :set -XTypeSynonymInstances @@ -27,7 +29,6 @@ >>> import Control.Lens hiding (Identity) >>> import Control.Lens.TH >>> import Data.Char ->>> import Test.DocTest >>> import Data.Singletons.TH (genSingletons) >>> import Data.Maybe @@ -295,3 +296,4 @@ module Data.Vinyl.Tutorial.Overview where import Data.Vinyl.Core import Data.Vinyl.Functor import Data.Vinyl.Lens +import Data.Singletons.TH (genSingletons) diff --git a/vinyl.cabal b/vinyl.cabal index 1676ae9..5e6736c 100644 --- a/vinyl.cabal +++ b/vinyl.cabal @@ -43,9 +43,14 @@ library build-depends: base >= 4.11 && <= 5, ghc-prim, deepseq, - array + array, + singletons if impl (ghc < 8.6.0) build-depends: constraints >= 0.6.1 + if impl (ghc < 9.0.1) + build-depends: singletons >= 0.10 && < 3 + else + build-depends: singletons-th >= 3 && < 3.1 default-language: Haskell2010 ghc-options: -Wall other-extensions: TypeApplications From 7bb7a3072c3bb62f05a86eed794035cadb317428 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 15 Jul 2023 11:38:15 +0200 Subject: [PATCH 05/54] align stack LTS with flake's ghc8107 --- stack.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/stack.yaml b/stack.yaml index 5c92dbd..6b2656e 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,4 +1,4 @@ -resolver: lts-17.8 +resolver: lts-18.28 packages: - . From a952fe2895b7de82958c0f0fbb4b829001d23a48 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 16 Jul 2023 11:47:21 +0200 Subject: [PATCH 06/54] add haskell language server to devShell --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index 419b5f9..d11528b 100644 --- a/flake.nix +++ b/flake.nix @@ -56,6 +56,7 @@ buildInputs = [ ghc hspkgs.cabal-install + hspkgs.haskell-language-server nurpkgs.repos.amesgen.cabal-docspec ]; }; From 2a623d98be6d661e7350944e9493bda2f871297e Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 16 Jul 2023 11:37:07 +0200 Subject: [PATCH 07/54] Add examples for Rec --- Data/Vinyl/Core.hs | 30 ++++++++++++++++++++++++++---- 1 file changed, 26 insertions(+), 4 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 9ca3cdc..a662ef1 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -57,10 +57,32 @@ import Control.DeepSeq (NFData, rnf) import Data.Constraint.Forall (Forall) #endif --- | A record is parameterized by a universe @u@, an interpretation @f@ and a --- list of rows @rs@. The labels or indices of the record are given by --- inhabitants of the kind @u@; the type of values at any label @r :: u@ is --- given by its interpretation @f r :: *@. +{- | +A record is parameterized by a universe @u@, an interpretation @f@ and a +list of rows @rs@. The labels or indices of the record are given by +inhabitants of the kind @u@; the type of values at any label @r :: u@ is +given by its interpretation @f r :: *@. + +>>> :set -XDataKinds +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> testRec = Identity 3 :& Identity "Hi" :& RNil +>>> :t testRec +testRec :: Num r => Rec Identity '[r, [Char]] +>>> testRec :: Rec Identity '[Int, String] +{3, "Hi"} + +>>> testRec = Just 3 :& Nothing :& Just "Hi" :& RNil +>>> :t testRec +testRec :: Num r1 => Rec Maybe '[r1, r2, [Char]] + +>>> :set -XTypeApplications +>>> import Data.Vinyl.Functor (ElField(Field)) +>>> testRec = Field @'("name", String) "Alice" :& Field @'("age", Int) 20 :& RNil +>>> :t testRec +testRec :: Rec ElField '[ '("name", String), '("age", Int)] +>>> testRec +{name :-> "Alice", age :-> 20} +-} data Rec :: (u -> *) -> [u] -> * where RNil :: Rec f '[] (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) From 02504591664fc8f0c543afedc80c0a44570c54ce Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 16 Jul 2023 11:43:34 +0200 Subject: [PATCH 08/54] add example for rappend --- Data/Vinyl/Core.hs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index a662ef1..020ce61 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -108,7 +108,16 @@ instance TestCoercion f => TestCoercion (Rec f) where Just Coercion testCoercion _ _ = Nothing --- | Two records may be pasted together. +{- | +Two records may be pasted together. + +>>> :set -XScopedTypeVariables +>>> testRec1 :: Rec Maybe '[Int, String] = Just 3 :& Just "Hi" :& RNil +>>> testRec2 :: Rec Maybe '[Double, [Double]] = Nothing :& Just [3.0, 2.2] :& RNil +>>> appendedTestRec = rappend testRec1 testRec2 +>>> :t appendedTestRec +appendedTestRec :: Rec Maybe '[Int, [Char], Double, [Double]] +-} rappend :: Rec f as -> Rec f bs From 84bbffa3ce5dbe2cf29a14587b7688804cbfc7a6 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 16 Jul 2023 11:45:29 +0200 Subject: [PATCH 09/54] add example for <+> --- Data/Vinyl/Core.hs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 020ce61..1d1d67f 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -125,7 +125,16 @@ rappend rappend RNil ys = ys rappend (x :& xs) ys = x :& (xs `rappend` ys) --- | A shorthand for 'rappend'. +{- | +A shorthand for 'rappend'. + +>>> :set -XScopedTypeVariables +>>> testRec1 :: Rec Maybe '[Int, String] = Just 3 :& Just "Hi" :& RNil +>>> testRec2 :: Rec Maybe '[Double, [Double]] = Nothing :& Just [3.0, 2.2] :& RNil +>>> appendedTestRecs = testRec1 <+> testRec2 +>>> :t appendedTestRecs +appendedTestRecs :: Rec Maybe '[Int, [Char], Double, [Double]] +-} (<+>) :: Rec f as -> Rec f bs From f918b3c12be17f26797d86db1b067fc60bb50a27 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 16 Jul 2023 12:48:07 +0200 Subject: [PATCH 10/54] Add example to rcombine --- Data/Vinyl/Core.hs | 36 +++++++++++++++++++++++++++++++----- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 1d1d67f..0e24306 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -141,11 +141,37 @@ appendedTestRecs :: Rec Maybe '[Int, [Char], Double, [Double]] -> Rec f (as ++ bs) (<+>) = rappend --- | Combine two records by combining their fields using the given --- function. The first argument is a binary operation for combining --- two values (e.g. '(<>)'), the second argument takes a record field --- into the type equipped with the desired operation, the third --- argument takes the combined value back to a result type. +{- | Combine two records by combining their fields using the given +function. The first argument is a binary operation for combining +two values (e.g. '(<>)'), the second argument takes a record field +into the type equipped with the desired operation, the third +argument takes the combined value back to a result type. + +This function makes no assumption on the types stored in the record and is thus +limited to basic operations that can be executed on all types (as defined via +the unconstrained forall a in arguments 1,2 and 3). The +following snippet shows how to put each entry of a Rec Maybe in a list +(second argument), concatenating them (first argument), and then outputting a +Rec [] instead of a Rec Maybe—something which can be done for any type: + +>>> import Data.Maybe (maybeToList) +>>> combineAsList = rcombine (<>) maybeToList id + +>>> testRec1 :: Rec Maybe '[String, String] = Just "Ho" :& Just "Hi" :& RNil +>>> combineAsList testRec1 testRec1 +{["Ho","Ho"], ["Hi","Hi"]} + +We can't combine testRec1 with rcombine such that the Strings would be +concatenated directly because that would make assumptions on the types and +violate the unconstrained forall a. However, we can use combineAsList now on +any other Rec Maybe as well. + +>>> testRec2 :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> combineAsList testRec2 testRec2 +{["Ho","Ho"], [3.0,3.0], []} + +-} + rcombine :: (RMap rs, RApply rs) => (forall a. m a -> m a -> m a) -> (forall a. f a -> m a) From 917799288e890e3117e9674d466ac3c3b144e28d Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:19 +0200 Subject: [PATCH 11/54] Add example for rmap --- Data/Vinyl/Core.hs | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 0e24306..9acab28 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -184,9 +184,22 @@ rcombine smash toM fromM x y = where x' = rmap toM x y' = rmap toM y --- | 'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u -> --- Hask@; that is, a natural transformation between two interpretation functors --- @f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@. +{- | +'Rec' @_ rs@ with labels in kind @u@ gives rise to a functor @Hask^u -> +Hask@; that is, a natural transformation between two interpretation functors +@f,g@ may be used to transport a value from 'Rec' @f rs@ to 'Rec' @g rs@. + +Here is an example: + +>>> import Data.Maybe (maybeToList) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> rmap maybeToList testRec +{["Ho"], [3.0], []} + +Similar to other functions in this module, we can not use rmap to map type +specific functions over a record. Only functions that work for any type can be +used. +-} class RMap rs where rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs From e23a74b3654c45b53425653060bccf7c26c0e805 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:37 +0200 Subject: [PATCH 12/54] add example for <<$>> --- Data/Vinyl/Core.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 9acab28..9ffcd5d 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -211,7 +211,12 @@ instance RMap xs => RMap (x ': xs) where rmap f (x :& xs) = f x :& rmap f xs {-# INLINE rmap #-} --- | A shorthand for 'rmap'. +{- | A shorthand for 'rmap'. +>>> import Data.Maybe (maybeToList) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> maybeToList <<$>> testRec +{["Ho"], [3.0], []} +-} (<<$>>) :: RMap rs => (forall x. f x -> g x) From 73cb2f783b5b28ed0cb36e5c788554b954f3e308 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:41 +0200 Subject: [PATCH 13/54] add example for <<&>> --- Data/Vinyl/Core.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 9ffcd5d..940265a 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -225,7 +225,12 @@ instance RMap xs => RMap (x ': xs) where (<<$>>) = rmap {-# INLINE (<<$>>) #-} --- | An inverted shorthand for 'rmap'. +{- | An inverted shorthand for 'rmap'. +>>> import Data.Maybe (maybeToList) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> testRec <<&>> maybeToList +{["Ho"], [3.0], []} +-} (<<&>>) :: RMap rs => Rec f rs From 78ae34ad00d6bfcb91bcc690506e9134c23df1a3 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:45 +0200 Subject: [PATCH 14/54] add example for rapply --- Data/Vinyl/Core.hs | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 940265a..971a2a9 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -239,8 +239,22 @@ instance RMap xs => RMap (x ': xs) where xs <<&>> f = rmap f xs {-# INLINE (<<&>>) #-} --- | A record of components @f r -> g r@ may be applied to a record of @f@ to --- get a record of @g@. +{- | +A record of components @f r -> g r@ may be applied to a record of @f@ to +get a record of @g@. + +>>> import Data.Vinyl.Functor (Const(Const), Lift(Lift)) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> :{ +funcRec = Lift (\x -> Const "String") + :& Lift (\x -> Const "Double") + :& Lift (\x -> Const "Int") + :& RNil +:} + +>>> recordToList $ rapply funcRec testRec +["String","Double","Int"] +-} class RApply rs where rapply :: Rec (Lift (->) f g) rs -> Rec f rs From e754df5a619963ff7c6141a2a9e5385a8267d2f8 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:48 +0200 Subject: [PATCH 15/54] add example for <<*>> --- Data/Vinyl/Core.hs | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 971a2a9..effd9b5 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -268,7 +268,21 @@ instance RApply xs => RApply (x ': xs) where rapply (f :& fs) (x :& xs) = getLift f x :& (fs `rapply` xs) {-# INLINE rapply #-} --- | A shorthand for 'rapply'. +{- | +A shorthand for 'rapply'. + +>>> import Data.Vinyl.Functor (Const(Const), Lift(Lift)) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> :{ +funcRec = Lift (\x -> Const "String") + :& Lift (\x -> Const "Double") + :& Lift (\x -> Const "Int") + :& RNil +:} + +>>> recordToList $ funcRec <<*>> testRec +["String","Double","Int"] +-} (<<*>>) :: RApply rs => Rec (Lift (->) f g) rs From bf3bfa35010730636422370d9e1941a47cb145cf Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:54 +0200 Subject: [PATCH 16/54] add example for rpure --- Data/Vinyl/Core.hs | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index effd9b5..101c547 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -291,8 +291,23 @@ funcRec = Lift (\x -> Const "String") (<<*>>) = rapply {-# INLINE (<<*>>) #-} --- | Given a section of some functor, records in that functor of any size are --- inhabited. +{- | +Given a section of some functor, records in that functor of any size are +inhabited. Note that you need a value that can inhabit any type in the record. +It is not possible, with this function, to derive a default with a type class +method. Here are a few examples: + +>>> testRec :: Rec Maybe '[Double, String] = rpure Nothing +>>> testRec +{Nothing, Nothing} +>>> testRec :: Rec [] '[Double, String] = rpure [] +>>> testRec +{[], []} +>>> import Data.Proxy (Proxy(Proxy)) +>>> testRec :: Rec Proxy '[Double, String] = rpure Proxy +>>> testRec +{Proxy, Proxy} +-} class RecApplicative rs where rpure :: (forall x. f x) From b5a26df9cbaaede848b7d31a10d3ac4c907f1758 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 19:51:59 +0200 Subject: [PATCH 17/54] add example for rtraverse --- Data/Vinyl/Core.hs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 101c547..f1fba40 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -319,9 +319,23 @@ instance RecApplicative rs => RecApplicative (r ': rs) where rpure s = s :& rpure s {-# INLINE rpure #-} --- | A record may be traversed with respect to its interpretation functor. This --- can be used to yank (some or all) effects from the fields of the record to --- the outside of the record. +{- | +A record may be traversed with respect to its interpretation functor. This +can be used to yank (some or all) effects from the fields of the record to +the outside of the record. + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> +:{ +ext :: Maybe x -> Maybe (Identity x) +ext (Just x) = Just (Identity x) +ext Nothing = Nothing +:} +>>> rtraverse ext testRec +Nothing +-} + rtraverse :: Applicative h => (forall x. f x -> h (g x)) From 7d294ae2556823b25b9a1c7f1dfcfdc96e5c5637 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 17 Jul 2023 20:03:19 +0200 Subject: [PATCH 18/54] add example for rtraverseIn --- Data/Vinyl/Core.hs | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index f1fba40..afc8c96 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -335,7 +335,6 @@ ext Nothing = Nothing >>> rtraverse ext testRec Nothing -} - rtraverse :: Applicative h => (forall x. f x -> h (g x)) @@ -345,13 +344,27 @@ rtraverse _ RNil = pure RNil rtraverse f (x :& xs) = (:&) <$> f x <*> rtraverse f xs {-# INLINABLE rtraverse #-} --- | While 'rtraverse' pulls the interpretation functor out of the --- record, 'rtraverseIn' pushes the interpretation functor in to each --- field type. This is particularly useful when you wish to discharge --- that interpretation on a per-field basis. For instance, rather than --- a @Rec IO '[a,b]@, you may wish to have a @Rec Identity '[IO a, IO --- b]@ so that you can evaluate a single field to obtain a value of --- type @Rec Identity '[a, IO b]@. +{- | +While 'rtraverse' pulls the interpretation functor out of the +record, 'rtraverseIn' pushes the interpretation functor in to each +field type. This is particularly useful when you wish to discharge +that interpretation on a per-field basis. For instance, rather than +a @Rec IO '[a,b]@, you may wish to have a @Rec Identity '[IO a, IO +b]@ so that you can evaluate a single field to obtain a value of +type @Rec Identity '[a, IO b]@. + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> testRec :: Rec Maybe '[String, Double, Int] = Just "Ho" :& Just 3.0 :& Nothing :& RNil +>>> +:{ +push :: forall x. Maybe x -> Identity (Maybe x) +push (Just x) = Identity (Just x) +push Nothing = Identity Nothing +:} +>>> :t rtraverseIn push testRec +rtraverseIn push testRec + :: Rec Identity '[Maybe [Char], Maybe Double, Maybe Int] +-} rtraverseIn :: forall h f g rs. (forall a. f a -> g (ApplyToField h a)) -> Rec f rs From 6c81e531bea15d937925ad500b15ae50a63f4df3 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Tue, 18 Jul 2023 09:49:30 +0200 Subject: [PATCH 19/54] add example for rsequenceIn --- Data/Vinyl/Core.hs | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index afc8c96..80e2e2c 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -373,7 +373,28 @@ rtraverseIn _ RNil = RNil rtraverseIn f (x :& xs) = f x :& rtraverseIn f xs {-# INLINABLE rtraverseIn #-} --- | Push an outer layer of interpretation functor into each field. +{- | +Push an outer layer of interpretation functor into each field. + +>>> :set -XTypeOperators +>>> import Data.Vinyl.Functor ((:.), Identity(Identity), Compose(Compose)) +:{ +testRec :: Rec (Maybe :. Identity) '[ String, Double, Int] = + Compose (Just (Identity "Ho")) + :& Compose (Just (Identity 3.0)) + :& Compose Nothing + :& RNil +:} +>>> :t rsequenceIn testRec +rsequenceIn testRec + :: Rec Identity '[Maybe [Char], Maybe Double, Maybe Int] + +Note that this function can't be applied as easily to anything +composed with interpretation functors as inner layer that take custom +kinds as inputs. For example, when dealing with (Maybe :. ElField), +Maybe the function can't be applied because that would require applying Maybe +to a (Symbol, *) kind. +-} rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g) => Rec (f :. g) rs -> Rec g (MapTyCon f rs) rsequenceIn = rtraverseIn @f (sequenceA . getCompose) From c00de1219348902d2815a6b0881c814ddd8341aa Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Tue, 18 Jul 2023 10:25:58 +0200 Subject: [PATCH 20/54] add another example for rtraverse --- Data/Vinyl/Core.hs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 80e2e2c..12031da 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -334,6 +334,23 @@ ext Nothing = Nothing :} >>> rtraverse ext testRec Nothing + +Here is another interesting example that allows reading a record +interactively. + +>>> :set -XTypeOperators +>>> import Text.Read (readMaybe) +>>> import Data.Vinyl.Functor ((:.), Compose(Compose), getCompose) +>>> +:{ +readMaybeIO :: forall a. Read a => (IO :. Maybe) a +readMaybeIO = Compose $ readMaybe <$> getLine +testRec :: Rec (IO :. Maybe) [String, Double, Int] +testRec = rpureConstrained @Read readMaybeIO +:} +>>> :t rtraverse getCompose testRec +rtraverse getCompose testRec + :: IO (Rec Maybe '[String, Double, Int]) -} rtraverse :: Applicative h From 66457a9255a4945f44dcfbcb1f381f2a1570cbd9 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 09:35:17 +0200 Subject: [PATCH 21/54] add another example for rtraverse --- Data/Vinyl/Core.hs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 12031da..4b0661b 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -351,6 +351,24 @@ testRec = rpureConstrained @Read readMaybeIO >>> :t rtraverse getCompose testRec rtraverse getCompose testRec :: IO (Rec Maybe '[String, Double, Int]) + +And one more with State + +>>> :set -package mtl +>>> import Control.Monad.State (StateT(StateT), runState, State, state) +>>> import qualified Data.Vinyl.Functor as V +>>> import qualified Data.Functor.Identity as I +>>> testRec1 :: Rec (State Int) '[Int, Double] = state (\s -> (s, 2 * s)) :& state (\s -> (fromIntegral s, 3 * s)) :& RNil +>>> +:{ +ext :: State Int a -> State Int (V.Identity a) +ext (StateT f) = StateT $ \s -> let (a, s') = I.runIdentity (f s) in I.Identity (V.Identity a, s') +:} +>>> stateRec = rtraverse ext testRec1 +>>> runState stateRec 1 +({1, 2.0},6) +>>> runState (sequence $ replicate 5 stateRec) 1 +([{1, 2.0},{6, 12.0},{36, 72.0},{216, 432.0},{1296, 2592.0}],7776) -} rtraverse :: Applicative h From 8d54d15d6a33d8f835c759550bd7bca2151c463e Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 09:44:59 +0200 Subject: [PATCH 22/54] add example for rzipWith --- Data/Vinyl/Core.hs | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 4b0661b..e535b7a 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -435,10 +435,18 @@ rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g) rsequenceIn = rtraverseIn @f (sequenceA . getCompose) {-# INLINABLE rsequenceIn #-} --- | Given a natural transformation from the product of @f@ and @g@ to @h@, we --- have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to --- @'Rec' h@. You can also think about this operation as zipping two records --- with the same element types but different interpretations. +{- | +Given a natural transformation from the product of @f@ and @g@ to @h@, we +have a natural transformation from the product of @'Rec' f@ and @'Rec' g@ to +@'Rec' h@. You can also think about this operation as zipping two records +with the same element types but different interpretations. + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> testRec1 :: Rec Identity '[String, Double] = Identity "Joe" :& Identity 20.0 :& RNil +>>> testRec2 :: Rec [] '[String, Double] = ["John"] :& [15.3] :& RNil +>>> rzipWith (\(Identity a) xs -> a:xs) testRec1 testRec2 +{["Joe","John"], [20.0,15.3]} +-} rzipWith :: (RMap xs, RApply xs) => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs rzipWith f = rapply . rmap (Lift . f) From 8c08a9419f4952ce43d3fd75a1ff6c035d322df0 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 10:04:40 +0200 Subject: [PATCH 23/54] add example for rfoldMap --- Data/Vinyl/Core.hs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index e535b7a..e210e71 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -467,6 +467,22 @@ instance RFoldMap xs => RFoldMap (x ': xs) where rfoldMapAux f m (r :& rs) = rfoldMapAux f (mappend m (f r)) rs {-# INLINE rfoldMapAux #-} +{- | +This function allows to collect all elements of a record in a monoid. The +collector function can be specialized for a particular interpretation functor +but has to be applicable for any type. It's therefore most useful to collect +effects. + +>>> testRec1 :: Rec Maybe '[String, Double] = Just "Anna" :& Nothing :& RNil +>>> +:{ +func :: forall x. Maybe x -> String +func (Just x) = "Just " +func Nothing = "Nothing " +:} +>>> rfoldMap func testRec1 +"Just Nothing " +-} rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs) => (forall x. f x -> m) -> Rec f rs -> m rfoldMap f = rfoldMapAux f mempty From 3d3276a06e1470d8158e82f2ad67034e9572f479 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 11:06:20 +0200 Subject: [PATCH 24/54] add example for Dict --- Data/Vinyl/Core.hs | 39 ++++++++++++++++++++++++++++++++++++++- 1 file changed, 38 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index e210e71..f917e1c 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -500,7 +500,44 @@ instance RecordToList xs => RecordToList (x ': xs) where recordToList (x :& xs) = getConst x : recordToList xs {-# INLINE recordToList #-} --- | Wrap up a value with a capability given by its type +{- | +Wrap up a value with a capability given by its type. In other words, the +existance of a value x :: Dict c a proves the existence of an instance c a. +This is useful to help the type checker realize that a value in a record does +indeed have a certain instance. + +To understand better why this type is useful, consider the following function +that doesn't typecheck: + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> import Data.Vinyl.TypeLevel (AllConstrained) +>>> +:{ +func :: forall rs. (RMap rs, AllConstrained Num rs) => Rec Identity rs -> Rec Identity rs +func = rmap (\(Identity x) -> Identity (x+1)) +:} +... + • Could not deduce (Num x) arising from a use of ‘+’ + from the context: (RMap rs, AllConstrained Num rs) + bound by the type signature for: + func :: forall (rs :: [*]). + (RMap rs, AllConstrained Num rs) => + Rec Identity rs -> Rec Identity rs +... + +Dict allows to encapsulate a constraint directly in the type such that anything +wrapped in it automatically fullfils it. RMap understands that as well: + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> +:{ +func :: forall rs. RMap rs => Rec (Dict Num) rs -> Rec Identity rs +func = rmap (\(Dict x) -> Identity (x + 1)) +:} +>>> testRec :: Rec (Dict Num) '[Double, Int] = Dict 1.0 :& Dict 0 :& RNil +>>> func testRec +{2.0, 1} +-} data Dict c a where Dict :: c a From c4f4d712b86468be20f071d12a4d9f996d7500b0 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 11:37:39 +0200 Subject: [PATCH 25/54] add example for reifyConstraint --- Data/Vinyl/Core.hs | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index f917e1c..a8ce156 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -544,11 +544,21 @@ data Dict c a where => a -> Dict c a --- | Sometimes we may know something for /all/ fields of a record, but when --- you expect to be able to /each/ of the fields, you are then out of luck. --- Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly, --- the constraint solver is not quite smart enough to realize this and we must --- make it patently obvious by reifying the constraint pointwise with proof. +{- | +Sometimes we may know something for /all/ fields of a record, but when +you expect to be able to /each/ of the fields, you are then out of luck. +Surely given @∀x:u.φ(x)@ we should be able to recover @x:u ⊢ φ(x)@! Sadly, +the constraint solver is not quite smart enough to realize this and we must +make it patently obvious by reifying the constraint pointwise with proof. + +Here is an example how this can be used in practise: + +>>> import Data.Vinyl.Functor (ElField(Field), Compose(Compose)) +>>> testRec :: Rec ElField '[ '("age", Double), '("number", Int)] = Field 1.0 :& Field 0 :& RNil +>>> testRecWithConstraints = reifyConstraint @Num testRec +>>> rmap (\(Compose (Dict x)) -> x+1) testRecWithConstraints +{age :-> 2.0, number :-> 1} +-} class ReifyConstraint c f rs where reifyConstraint :: Rec f rs From e5acb28b0e56001cf22ec83dbee08b4d90e80333 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Fri, 21 Jul 2023 11:58:40 +0200 Subject: [PATCH 26/54] add example for rpureConstrained --- Data/Vinyl/Core.hs | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index a8ce156..d1675bd 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -573,8 +573,27 @@ instance (c (f x), ReifyConstraint c f xs) reifyConstraint (x :& xs) = Compose (Dict x) :& reifyConstraint xs {-# INLINE reifyConstraint #-} --- | Build a record whose elements are derived solely from a --- constraint satisfied by each. +{- | +Build a record whose elements are derived solely from a +constraint satisfied by each. + +>>> :set -XFlexibleInstances +>>> :set -XFlexibleContexts +>>> :set -XUndecidableInstances +>>> import Data.Vinyl.Derived (KnownField) +>>> import Data.Vinyl.TypeLevel (Snd) +>>> import Data.Vinyl.Functor (ElField(Field)) +>>> import Data.Proxy (Proxy(Proxy)) +>>> class (KnownField a, Monoid (Snd a)) => Helper a +>>> instance (KnownField a, Monoid (Snd a)) => Helper a +>>> +:{ +testRec :: Rec ElField '[ '("list", [Double]), '("string", String) ] +testRec = rpureConstrained @Helper (Field mempty) +:} +>>> testRec +{list :-> [], string :-> ""} +-} class RPureConstrained c ts where rpureConstrained :: (forall a. c a => f a) -> Rec f ts From b2d4a0c111b020fb601cced0cececc6c3fa63c08 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 29 Jul 2023 10:53:11 +0200 Subject: [PATCH 27/54] add example for DictOnly --- Data/Vinyl/Core.hs | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index d1675bd..bb804fc 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -605,9 +605,43 @@ instance (c x, RPureConstrained c xs) => RPureConstrained c (x ': xs) where rpureConstrained f = f :& rpureConstrained @c @xs f {-# INLINE rpureConstrained #-} --- | Capture a type class instance dictionary. See --- 'Data.Vinyl.Lens.getDict' for a way to obtain a 'DictOnly' value --- from an 'RPureConstrained' constraint. +{- | +Capture a type class instance dictionary. This data type can +be used together with rpureConstrained: + +>>> import Data.Vinyl.Lens (rget) +>>> +:{ +testRec :: Rec (DictOnly Num) '[Double, Int] +testRec = rpureConstrained @Num @'[Double, Int] DictOnly +:} +>>> +:{ +val :: DictOnly Num Double +val = rget @Double testRec +:} + +In itself not much can be done with a @DictOnly@. However, +it becomes useful together with the @Product@ Functor that allows +to pair it on the side with another value. That way we can keep +track of a constraint and use the other value for computations: + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> import Data.Functor.Product (Product(Pair)) +>>> +:{ +builder :: Num a => Product (DictOnly Num) Identity a +builder = Pair DictOnly (Identity 0) +:} +>>> +:{ +testRec :: Rec (Product (DictOnly Num) Identity) '[Double, Int] +testRec = rpureConstrained @Num @'[Double, Int] builder +:} +>>> Pair DictOnly val = rget @Double testRec +>>> val +0.0 +-} data DictOnly (c :: k -> Constraint) a where DictOnly :: forall c a. c a => DictOnly c a From 6933ce70c99b1a1ba16f696b22ee259e93e7f6fa Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 29 Jul 2023 11:34:25 +0200 Subject: [PATCH 28/54] add example for withPairedDict --- Data/Vinyl/Core.hs | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index bb804fc..1f6c2ef 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -645,9 +645,22 @@ testRec = rpureConstrained @Num @'[Double, Int] builder data DictOnly (c :: k -> Constraint) a where DictOnly :: forall c a. c a => DictOnly c a --- | A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on --- a 'Rec' to pair each field with a type class dictionary for --- @MyClass@. This helper can then be used to eliminate the original. +{- | +A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on a 'Rec' to +pair each field with a type class dictionary for @MyClass@. This helper can +then be used to apply a function to a DictOnly that is paired with another +field: + +>>> import Data.Vinyl.Functor (Identity(Identity)) +>>> import Data.Functor.Product (Product(Pair)) +>>> +:{ +testRec :: Rec (Product (DictOnly Num) Identity) '[Double, Int] +testRec = rpureConstrained @Num @'[Double, Int] (Pair DictOnly (Identity 0)) +:} +>>> rmap (withPairedDict (fmap (2 +))) testRec +{2.0, 2} +-} withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r withPairedDict f (Pair DictOnly x) = f x From bad733c210ceb85d33cc1f602d5e619b1e3fd98d Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 21:58:12 +0200 Subject: [PATCH 29/54] add example for data Nat --- Data/Vinyl/TypeLevel.hs | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 70b00e9..e5fa685 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -24,8 +24,27 @@ module Data.Vinyl.TypeLevel where import Data.Coerce import Data.Kind --- | A mere approximation of the natural numbers. And their image as lifted by --- @-XDataKinds@ corresponds to the actual natural numbers. +{- | +A mere approximation of the natural numbers. And their image as lifted by +@-XDataKinds@ corresponds to the actual natural numbers. + +The following is an example for a term level number of type Nat: + +>>> number = S (S Z) +>>> :t number +number :: Nat + +But it is intended to be used at the type level: + +>>> import Data.Proxy (Proxy(Proxy)) +>>> Proxy :: Proxy (S (S Z)) +Proxy + +Often it is used with type applications: + +>>> Proxy @(S (S Z)) +Proxy +-} data Nat = Z | S !Nat -- | Produce a runtime 'Int' value corresponding to a 'Nat' type. From 00428bc61de70843efad0ccec505110dc5d6423a Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 21:59:54 +0200 Subject: [PATCH 30/54] add example for natToInt --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index e5fa685..f84ae1e 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -47,7 +47,13 @@ Proxy -} data Nat = Z | S !Nat --- | Produce a runtime 'Int' value corresponding to a 'Nat' type. +{- | +Produce a runtime 'Int' value corresponding to a 'Nat' type. +This is intended to be used with TypeApplications: + +>>> natToInt @('S ('S 'Z)) +2 +-} class NatToInt (n :: Nat) where natToInt :: Int From 648642d52879ea26dc608dda59aa17d79215f23c Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:08:51 +0200 Subject: [PATCH 31/54] add example for indexWitnesses --- Data/Vinyl/TypeLevel.hs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index f84ae1e..2b75896 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -65,8 +65,13 @@ instance NatToInt n => NatToInt ('S n) where natToInt = 1 + natToInt @n {-# INLINE natToInt #-} --- | Reify a list of type-level natural number indices as runtime --- 'Int's relying on instances of 'NatToInt'. +{- | +Reify a list of type-level natural number indices as runtime +'Int's relying on instances of 'NatToInt'. + +>>> indexWitnesses @'[S (S Z), Z, S (S (S Z))] +[2,0,3] +-} class IndexWitnesses (is :: [Nat]) where indexWitnesses :: [Int] From 4e52eafb5cfb7b7b78ce7ecff2f1f0953b8b0798 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:16:43 +0200 Subject: [PATCH 32/54] add example for Fst --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 2b75896..6645f81 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -83,7 +83,13 @@ instance (IndexWitnesses is, NatToInt i) => IndexWitnesses (i ': is) where indexWitnesses = natToInt @i : indexWitnesses @is {-# INLINE indexWitnesses #-} --- | Project the first component of a type-level tuple. +{- | +Project the first component of a type-level tuple. + +>>> :k! Fst '("age", Int) +Fst '("age", Int) :: GHC.Types.Symbol += "age" +-} type family Fst (a :: (k1,k2)) where Fst '(x,y) = x -- | Project the second component of a type-level tuple. From 110b7705ed0ab6dab1b3612de7478c7f12dfeb58 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:17:56 +0200 Subject: [PATCH 33/54] add example for Snd --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 6645f81..4ddde87 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -92,7 +92,13 @@ Fst '("age", Int) :: GHC.Types.Symbol -} type family Fst (a :: (k1,k2)) where Fst '(x,y) = x --- | Project the second component of a type-level tuple. +{- | +Project the second component of a type-level tuple. + +>>> :k! Snd '("age", Int) +Snd '("age", Int) :: * += Int +-} type family Snd (a :: (k1,k2)) where Snd '(x,y) = y type family RLength xs where From 64b76311f8992de713ffa6d238c846dc79cfb5bd Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:22:35 +0200 Subject: [PATCH 34/54] add example for RLength --- Data/Vinyl/TypeLevel.hs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 4ddde87..a4c487c 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -101,6 +101,13 @@ Snd '("age", Int) :: * -} type family Snd (a :: (k1,k2)) where Snd '(x,y) = y +{- | +Compute the length of a type level list. + +>>> :k! RLength '[ '("age", Int), '("name", String)] +RLength '[ '("age", Int), '("name", String)] :: Nat += 'S ('S 'Z) +-} type family RLength xs where RLength '[] = 'Z RLength (x ': xs) = 'S (RLength xs) From 5073173a9b5dd7f7b92282bb37375495cf599327 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:33:19 +0200 Subject: [PATCH 35/54] add example for RIndex --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index a4c487c..b05bdb2 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -112,7 +112,13 @@ type family RLength xs where RLength '[] = 'Z RLength (x ': xs) = 'S (RLength xs) --- | A partial relation that gives the index of a value in a list. +{- | +Compute the index of a value in a list. + +>>> :k! RIndex '("age", Int) '[ '("age", Int), '("name", String)] +RIndex '("age", Int) '[ '("age", Int), '("name", String)] :: Nat += 'Z +-} type family RIndex (r :: k) (rs :: [k]) :: Nat where RIndex r (r ': rs) = 'Z RIndex r (s ': rs) = 'S (RIndex r rs) From 608be6aee88dcfb2bccf4009496457c35f79ccac Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:33:37 +0200 Subject: [PATCH 36/54] add example for RImage --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index b05bdb2..3e1778f 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -123,7 +123,13 @@ type family RIndex (r :: k) (rs :: [k]) :: Nat where RIndex r (r ': rs) = 'Z RIndex r (s ': rs) = 'S (RIndex r rs) --- | A partial relation that gives the indices of a sublist in a larger list. +{- | +Compute the indices of a sublist in a larger list. + +>>> :k! RImage '[Int, String] '[Int, Double, String] +RImage '[Int, String] '[Int, Double, String] :: [Nat] += '[ 'Z, 'S ('S 'Z)] +-} type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where RImage '[] ss = '[] RImage (r ': rs) ss = RIndex r ss ': RImage rs ss From 96c78815ee582100289de49df577bd1fac39afaa Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sun, 30 Jul 2023 22:35:12 +0200 Subject: [PATCH 37/54] add example for RDelete --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 3e1778f..f122d17 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -134,7 +134,13 @@ type family RImage (rs :: [k]) (ss :: [k]) :: [Nat] where RImage '[] ss = '[] RImage (r ': rs) ss = RIndex r ss ': RImage rs ss --- | Remove the first occurrence of a type from a type-level list. +{- | +Remove the first occurrence of a type from a type-level list. + +>>> :k! RDelete Int '[Int, Double, String] +RDelete Int '[Int, Double, String] :: [*] += '[Double, String] +-} type family RDelete r rs where RDelete r (r ': rs) = rs RDelete r (s ': rs) = s ': RDelete r rs From 0cb5b0a6f161262ff7ee48508ed6b3dd7b574599 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 31 Jul 2023 14:26:57 +0200 Subject: [PATCH 38/54] add example for RecAll --- Data/Vinyl/TypeLevel.hs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index f122d17..6e2fda6 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -145,7 +145,16 @@ type family RDelete r rs where RDelete r (r ': rs) = rs RDelete r (s ': rs) = s ': RDelete r rs --- | A constraint-former which applies to every field in a record. +{- | +Build a constraint tuple with one constraint for every field +in a record. + +>>> import Data.Vinyl.Functor (ElField) +>>> :k! RecAll ElField '[ '("age", Int), '("name", Double)] Num +RecAll ElField '[ '("age", Int), '("name", Double)] Num :: Constraint += (Num (ElField '("age", Int)), + (Num (ElField '("name", Double)), () :: Constraint)) +-} type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constraint where RecAll f '[] c = () RecAll f (r ': rs) c = (c (f r), RecAll f rs c) From 9dafd37133bd749a0ae2cff2085ba6aa1d6f9ec7 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Mon, 31 Jul 2023 14:31:04 +0200 Subject: [PATCH 39/54] add example for (++) --- Data/Vinyl/TypeLevel.hs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 6e2fda6..1ecc0ed 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -161,7 +161,13 @@ type family RecAll (f :: u -> *) (rs :: [u]) (c :: * -> Constraint) :: Constrain infixr 5 ++ --- | Append for type-level lists. +{- | +Append for type-level lists. + +>>> :k! '[Int, Double] ++ '[String] +'[Int, Double] ++ '[String] :: [*] += '[Int, Double, String] +-} type family (as :: [k]) ++ (bs :: [k]) :: [k] where '[] ++ bs = bs (a ': as) ++ bs = a ': (as ++ bs) From 358f50f25cc6caff3750f1e467223f4955615e1c Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 10:31:28 +0200 Subject: [PATCH 40/54] add example for AllConstrained --- Data/Vinyl/TypeLevel.hs | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 1ecc0ed..be2406d 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -172,8 +172,22 @@ type family (as :: [k]) ++ (bs :: [k]) :: [k] where '[] ++ bs = bs (a ': as) ++ bs = a ': (as ++ bs) --- | Constraint that all types in a type-level list satisfy a --- constraint. +{- | +Constraint that all types in a type-level list satisfy a +constraint. + +>>> :k! AllConstrained Num '[Int, Double] +AllConstrained Num '[Int, Double] :: Constraint += (Num Int, (Num Double, () :: Constraint)) + +>>> +:{ +f :: AllConstrained Num '[a, b] => Either a b +f = Right 0 +:} +>>> f :: Either Double Int +Right 0 +-} type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint where AllConstrained c '[] = () AllConstrained c (t ': ts) = (c t, AllConstrained c ts) From 762d30e1e5184d59984109282143fa953472b156 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 11:24:49 +0200 Subject: [PATCH 41/54] illustrate issue with AllSatisfied class --- Data/Vinyl/TypeLevel.hs | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index be2406d..f85de26 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -192,8 +192,24 @@ type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint wher AllConstrained c '[] = () AllConstrained c (t ': ts) = (c t, AllConstrained c ts) --- | Constraint that each Constraint in a type-level list is satisfied --- by a particular type. +{- | +Constraint that each Constraint in a type-level list is satisfied by a +particular type. This class is of limited use: Although it is required that the +type has all instances for each of the constraints, this +"for each" information is lost by ghc as the following example illustrates: + +>>> +:{ +f :: AllSatisfied '[Num, Eq, Show] a => a -> String +f a = if a == 0 then show a else "not equal to 0" +:} +... + • Could not deduce (Eq a) arising from a use of ‘==’ + from the context: AllSatisfied '[Num, Eq, Show] a + bound by the type signature for: + f :: forall a. AllSatisfied '[Num, Eq, Show] a => a -> String +... +-} class AllSatisfied cs t where instance AllSatisfied '[] t where instance (c t, AllSatisfied cs t) => AllSatisfied (c ': cs) t where From 52991fd5a07c6f629f2748e0f9992a0bd46b32f4 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 11:27:53 +0200 Subject: [PATCH 42/54] add AllSatisfied', alternative for AllSatisfied The alternative is computed as type family not as class. The latter doesn't seem to work. --- Data/Vinyl/TypeLevel.hs | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index f85de26..afa6409 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -192,6 +192,20 @@ type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint wher AllConstrained c '[] = () AllConstrained c (t ': ts) = (c t, AllConstrained c ts) +{- | +Alternative to get a constraint that each Constraint in a type-level list is +satisfied by a particular type. + +>>> +:{ +f :: AllSatisfied' '[Num, Eq, Show] a => a -> String +f a = if a == 0 then show a else "not equal to 0" +:} +-} +type family AllSatisfied' (cs :: [u -> Constraint]) (t :: u) :: Constraint where + AllSatisfied' '[] t = () + AllSatisfied' (c ': cs) t = (c t, AllSatisfied' cs t) + {- | Constraint that each Constraint in a type-level list is satisfied by a particular type. This class is of limited use: Although it is required that the From 1342969b0f73b04fc21a2c8f72d4fb41b4c5d1fe Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 11:35:05 +0200 Subject: [PATCH 43/54] replace AllSatisfied with AllSatisfied' --- Data/Vinyl/TypeLevel.hs | 28 +++------------------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index afa6409..86e096c 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -196,37 +196,15 @@ type family AllConstrained (c :: u -> Constraint) (ts :: [u]) :: Constraint wher Alternative to get a constraint that each Constraint in a type-level list is satisfied by a particular type. ->>> -:{ -f :: AllSatisfied' '[Num, Eq, Show] a => a -> String -f a = if a == 0 then show a else "not equal to 0" -:} --} -type family AllSatisfied' (cs :: [u -> Constraint]) (t :: u) :: Constraint where - AllSatisfied' '[] t = () - AllSatisfied' (c ': cs) t = (c t, AllSatisfied' cs t) - -{- | -Constraint that each Constraint in a type-level list is satisfied by a -particular type. This class is of limited use: Although it is required that the -type has all instances for each of the constraints, this -"for each" information is lost by ghc as the following example illustrates: - >>> :{ f :: AllSatisfied '[Num, Eq, Show] a => a -> String f a = if a == 0 then show a else "not equal to 0" :} -... - • Could not deduce (Eq a) arising from a use of ‘==’ - from the context: AllSatisfied '[Num, Eq, Show] a - bound by the type signature for: - f :: forall a. AllSatisfied '[Num, Eq, Show] a => a -> String -... -} -class AllSatisfied cs t where -instance AllSatisfied '[] t where -instance (c t, AllSatisfied cs t) => AllSatisfied (c ': cs) t where +type family AllSatisfied (cs :: [u -> Constraint]) (t :: u) :: Constraint where + AllSatisfied '[] t = () + AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t) -- | Constraint that all types in a type-level list satisfy each -- constraint from a list of constraints. From c79fe77896096a5876009e3f34ce99fb35015398 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 11:37:03 +0200 Subject: [PATCH 44/54] add example for AllAllSat --- Data/Vinyl/TypeLevel.hs | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/Data/Vinyl/TypeLevel.hs b/Data/Vinyl/TypeLevel.hs index 86e096c..9a44e3f 100644 --- a/Data/Vinyl/TypeLevel.hs +++ b/Data/Vinyl/TypeLevel.hs @@ -206,12 +206,22 @@ type family AllSatisfied (cs :: [u -> Constraint]) (t :: u) :: Constraint where AllSatisfied '[] t = () AllSatisfied (c ': cs) t = (c t, AllSatisfied cs t) --- | Constraint that all types in a type-level list satisfy each --- constraint from a list of constraints. --- --- @AllAllSat cs ts@ should be equivalent to @AllConstrained --- (AllSatisfied cs) ts@ if partial application of type families were --- legal. +{- | +Constraint that all types in a type-level list satisfy each +constraint from a list of constraints. + +@AllAllSat cs ts@ should be equivalent to @AllConstrained +(AllSatisfied cs) ts@ if partial application of type families were +legal. + +>>> +:{ +f :: AllAllSat '[Num, Eq, Show] '[a, b] => a -> b -> (String, Bool) +f a b = (if a == 0 then show a else "not equal to 0", b == 0) +:} +>>> f (0 :: Int) (1.0 :: Double) +("0",False) +-} type family AllAllSat cs ts :: Constraint where AllAllSat cs '[] = () AllAllSat cs (t ': ts) = (AllSatisfied cs t, AllAllSat cs ts) From b9d0d86e9e1a54b0e6092ae73c0c074db32a7061 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 14:58:30 +0200 Subject: [PATCH 45/54] add example for rpureConstraints --- Data/Vinyl/Core.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 1f6c2ef..647b176 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -664,8 +664,14 @@ testRec = rpureConstrained @Num @'[Double, Int] (Pair DictOnly (Identity 0)) withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r withPairedDict f (Pair DictOnly x) = f x --- | Build a record whose elements are derived solely from a --- list of constraint constructors satisfied by each. +{- | +Build a record whose elements are derived solely from a +list of constraint constructors satisfied by each. + +>>> import Data.Functor.Identity (Identity(Identity)) +>>> rpureConstraints @'[Num, Enum] (succ (Identity 0)) :: Rec Identity '[Int, Double] +{Identity 1, Identity 1.0} +-} class RPureConstraints cs ts where rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts From f68ee13b329deee29977b162e4fc921f9b8cd750 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 15:21:30 +0200 Subject: [PATCH 46/54] example for show instance --- Data/Vinyl/Core.hs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 647b176..7632d37 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -684,8 +684,13 @@ instance (AllSatisfied cs t, RPureConstraints cs ts) rpureConstraints f = f :& rpureConstraints @cs @ts f {-# INLINE rpureConstraints #-} --- | Records may be shown insofar as their points may be shown. --- 'reifyConstraint' is used to great effect here. +{- | +Records may be shown insofar as their points may be shown. +'reifyConstraint' is used to great effect here. + +>>> "record with Nothings: " ++ (show (rpure Nothing :: Rec Maybe '[Int, Double])) +"record with Nothings: {Nothing, Nothing}" +-} instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs) where show xs = From 14737a1ce3f911544fa93848ffcb4737442ab6c8 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 15:21:46 +0200 Subject: [PATCH 47/54] example for Semigroup instance --- Data/Vinyl/Core.hs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 7632d37..b74e64e 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -700,6 +700,14 @@ instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs) . rmap (\(Compose (Dict x)) -> Const $ show x) $ reifyConstraint @Show xs +{- | +The Semigroup instance is mapped to each element of the record. + +>>> t1 = ["Alice", "Bob"] :& [20, 22] :& RNil +>>> t2 = ["Charlie", "Dan"] :& [24, 23] :& RNil +>>> t1 <> t2 +{["Alice","Bob","Charlie","Dan"], [20,22,24,23]} +-} instance Semigroup (Rec f '[]) where RNil <> RNil = RNil From 9b42df96d480123fd481a6a616fcdc226e12be84 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 15:22:00 +0200 Subject: [PATCH 48/54] example for Monoid instance --- Data/Vinyl/Core.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index b74e64e..e032919 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -715,6 +715,12 @@ instance (Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs)) where (x :& xs) <> (y :& ys) = (x <> y) :& (xs <> ys) +{- | +The Monoid instance is also mapped to each element of the record. + +>>> mempty :: Rec [] '[Double, String, Int] +{[], [], []} +-} instance Monoid (Rec f '[]) where mempty = RNil RNil `mappend` RNil = RNil From 5c237c3fc723d95ce4cd37ba30e3bf9dfa5a010f Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 15:27:11 +0200 Subject: [PATCH 49/54] add example for Eq instance --- Data/Vinyl/Core.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index e032919..86e4dc8 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -729,6 +729,15 @@ instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where mempty = mempty :& mempty (x :& xs) `mappend` (y :& ys) = (mappend x y) :& (mappend xs ys) +{- | +The Eq instance is also just an element-wise comparison. + +>>> import Data.Vinyl.Functor (ElField(Field)) +>>> r1 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Alice":& Field 30 :& RNil +>>> r2 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Bob":& Field 25 :& RNil +>>> r1 == r2 +False +-} instance Eq (Rec f '[]) where _ == _ = True instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where From a7f3143b767222d2e619638eba7500449dc32699 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 20:21:20 +0200 Subject: [PATCH 50/54] add example for Ord instance --- Data/Vinyl/Core.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 86e4dc8..7dece1f 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -743,6 +743,16 @@ instance Eq (Rec f '[]) where instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where (x :& xs) == (y :& ys) = (x == y) && (xs == ys) +{- | +The Ord instance is element-wise, lexicographical ordering using the Monoid +instance of the Ordering type. + +>>> import Data.Vinyl.Functor (ElField(Field)) +>>> r1 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Alice":& Field 30 :& RNil +>>> r2 :: Rec ElField '[ '("name", String), '("age", Int)] = Field "Bob":& Field 25 :& RNil +>>> r1 < r2 +True +-} instance Ord (Rec f '[]) where compare _ _ = EQ instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where From 21d6ed0101f711ae92afd30c215eef0a54d232a0 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 20:28:31 +0200 Subject: [PATCH 51/54] add example for Head --- Data/Vinyl/Core.hs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 7dece1f..997a7c4 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -811,11 +811,17 @@ instance ReifyConstraint NFData f xs => NFData (Rec f xs) where go RNil = () go (Compose (Dict x) :& xs) = rnf x `seq` go xs --- | Analogous to 'Data.List.head'. Unlike the version in @singletons@, --- this family merely gets stuck instead of producing a type error if --- the list is empty. This is often better, because the type error that --- would be produced here would be much less informative than one that --- would likely be available where it's used. +{- | +Analogous to 'Data.List.head'. Unlike the version in @singletons@, +this family merely gets stuck instead of producing a type error if +the list is empty. This is often better, because the type error that +would be produced here would be much less informative than one that +would likely be available where it's used. + +>>> :k! Head '[Int, Double, String] +Head '[Int, Double, String] :: * += Int +-} type family Head xs where Head (x ': _) = x From 6d39093ad7aa68f0b623487b54dbf5e33905b2e3 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Wed, 2 Aug 2023 20:30:42 +0200 Subject: [PATCH 52/54] add example for Tail --- Data/Vinyl/Core.hs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Data/Vinyl/Core.hs b/Data/Vinyl/Core.hs index 997a7c4..20057e5 100644 --- a/Data/Vinyl/Core.hs +++ b/Data/Vinyl/Core.hs @@ -825,11 +825,17 @@ Head '[Int, Double, String] :: * type family Head xs where Head (x ': _) = x --- | Analogous to 'Data.List.tail'. Unlike the version in @singletons@, --- this family merely gets stuck instead of producing a type error if --- the list is empty. This is often better, because the type error that --- would be produced here would be much less informative than one that --- would likely be available where it's used. +{- | +Analogous to 'Data.List.tail'. Unlike the version in @singletons@, +this family merely gets stuck instead of producing a type error if +the list is empty. This is often better, because the type error that +would be produced here would be much less informative than one that +would likely be available where it's used. + +>>> :k! Tail '[Int, Double, String] +Tail '[Int, Double, String] :: [*] += '[Double, String] +-} type family Tail xs where Tail (_ ': xs) = xs From 30e8e59f8ba2eeab1baccd4ddc619f87372285fb Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 28 Oct 2023 09:24:47 +0200 Subject: [PATCH 53/54] remove doctest dependency --- Data/Vinyl/Tutorial/Overview.hs | 2 - tests/Intro.lhs | 291 -------------------------------- tests/doctests.hs | 18 +- vinyl.cabal | 33 ++-- 4 files changed, 22 insertions(+), 322 deletions(-) delete mode 100644 tests/Intro.lhs diff --git a/Data/Vinyl/Tutorial/Overview.hs b/Data/Vinyl/Tutorial/Overview.hs index 568b7c7..203b355 100644 --- a/Data/Vinyl/Tutorial/Overview.hs +++ b/Data/Vinyl/Tutorial/Overview.hs @@ -295,5 +295,3 @@ module Data.Vinyl.Tutorial.Overview where import Data.Vinyl.Core import Data.Vinyl.Functor -import Data.Vinyl.Lens -import Data.Singletons.TH (genSingletons) diff --git a/tests/Intro.lhs b/tests/Intro.lhs deleted file mode 100644 index 7c5ef9d..0000000 --- a/tests/Intro.lhs +++ /dev/null @@ -1,291 +0,0 @@ -This introduction was originally published at - - -Vinyl: Modern Records for Haskell -================================= - -Vinyl is a general solution to the records problem in Haskell using -type level strings and other modern GHC features, featuring static -structural typing (with a subtyping relation), and automatic -row-polymorphic lenses. All this is possible without Template Haskell. - -First, install Vinyl from Hackage: - -< cabal update -< cabal install vinyl singletons - -Let’s work through a quick example. We’ll need to enable some language -extensions first: - -> {-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-} -> {-# LANGUAGE FlexibleContexts, FlexibleInstances, NoMonomorphismRestriction #-} -> {-# LANGUAGE GADTs, TypeSynonymInstances, TemplateHaskell, StandaloneDeriving #-} -> {-# LANGUAGE TypeApplications #-} -> {-# LANGUAGE CPP #-} -#if __GLASGOW_HASKELL__ >= 810 -> {-# LANGUAGE StandaloneKindSignatures #-} -#endif - -> module Intro where -> import Data.Vinyl -> import Data.Vinyl.Functor -> import Control.Lens hiding (Identity) -> import Data.Char -> import Test.DocTest -> import Data.Singletons.TH (genSingletons) - -Let’s define a universe of fields which we want to use. - -First of all, we need a data type defining the field labels: - -> data Fields = Name | Age | Sleeping | Master deriving Show - -Any record can be now described by a type-level list of these labels. -The `DataKinds` extension must be enabled to automatically turn all the -constructors of the `Field` type into types. - -> type LifeForm = [Name, Age, Sleeping] - -Now, we need a way to map our labels to concrete types. We use a type -family for this purpose: - -> type family ElF (f :: Fields) :: * where -> ElF Name = String -> ElF Age = Int -> ElF Sleeping = Bool -> ElF Master = Rec Attr LifeForm - -Unfortunately, type families aren't first class in Haskell. That's -why we also need a data type, with which we will parametrise `Rec`: - -> newtype Attr f = Attr { _unAttr :: ElF f } -> makeLenses ''Attr -> instance Show (Attr Name) where show (Attr x) = "name: " ++ show x -> instance Show (Attr Age) where show (Attr x) = "age: " ++ show x -> instance Show (Attr Sleeping) where show (Attr x) = "sleeping: " ++ show x -> instance Show (Attr Master) where show (Attr x) = "master: " ++ show x - -To make field construction easier, we define an operator. The first -argument of this operator is a singleton - a constructor bringing the -data-kinded field label type into the data level. It's needed because -there can be multiple labels with the same field type, so by just -supplying a value of type `ElF f` there would be no way to deduce the -correct `f`. - -> (=::) :: sing f -> ElF f -> Attr f -> _ =:: x = Attr x - -We generate the necessary singletons for each field label using -Template Haskell: - -> genSingletons [ ''Fields ] - -Now, let’s try to make an entity that represents a human: - -> jon = (SName =:: "jon") -> :& (SAge =:: 23) -> :& (SSleeping =:: False) -> :& RNil - -Automatically, we can show the record: - -> -- | -> -- >>> show jon -> -- "{name: \"jon\", age: 23, sleeping: False}" - -And its types are all inferred with no problem. Now, make a dog! Dogs -are life-forms, but unlike humans, they have masters. So, let’s build -my dog: - -> tucker = (SName =:: "tucker") -> :& (SAge =:: 9) -> :& (SSleeping =:: True) -> :& (SMaster =:: jon) -> :& RNil - -Using Lenses ------------- - -Now, if we want to wake entities up, we don’t want to have to write a -separate wake-up function for both dogs and humans (even though they -are of different type). Luckily, we can use the built-in lenses to -focus on a particular field in the record for access and update, -without losing additional information: - - -> wakeUp :: (Sleeping ∈ fields) => Rec Attr fields -> Rec Attr fields -> wakeUp = rput $ SSleeping =:: False - -Now, the type annotation on `wakeUp` was not necessary; I just wanted -to show how intuitive the type is. Basically, it takes as an input -any record that has a `Bool` field labelled `sleeping`, and modifies -that specific field in the record accordingly. - -> tucker' = wakeUp tucker -> jon' = wakeUp jon - -> -- | -> -- >>> :set -XTypeApplications -XDataKinds -> -- >>> tucker' ^. rlens @Sleeping -> -- sleeping: False -> -- -> -- >>> tucker ^. rlens @Sleeping -> -- sleeping: True -> -- -> -- >>> jon' ^. rlens @Sleeping -> -- sleeping: False - -We can also access the entire lens for a field using the rLens -function; since lenses are composable, it’s super easy to do deep -update on a record: - -> masterSleeping = rlens @Master . unAttr . rlens @Sleeping -> tucker'' = masterSleeping .~ (SSleeping =:: True) $ tucker' - -> -- | >>> tucker'' ^. masterSleeping -> -- sleeping: True - -Subtyping Relation and Coercion -------------------------------- - -A record `Rec f xs` is a subtype of a record `Rec f ys` if `ys ⊆ xs`; -that is to say, if one record can do everything that another record -can, the former is a subtype of the latter. As such, we should be able -to provide an upcast operator which “forgets” whatever makes one -record different from another (whether it be extra data, or different -order). - -Therefore, the following works: - -> upcastedTucker :: Rec Attr LifeForm -> upcastedTucker = rcast tucker - -The subtyping relationship between record types is expressed with the -`(<:)` constraint; so, `rcast` is of the following type: - -< rcast :: r1 <: r2 => Rec f r1 -> Rec f r2 - -Also provided is a `(≅)` constraint which indicates record congruence -(that is, two record types differ only in the order of their fields). - -In fact, `rcast` is actually given as a special case of the lens `rsubset`, -which lets you modify entire (possibly non-contiguous) slices of a record! - -Records are polymorphic over functors -------------------------------------- - -Consider the following declaration: - -< data Rec :: (u -> *) -> [u] -> * where -< RNil :: Rec f '[] -< (:&) :: f r -> Rec f rs -> Rec f (r ': rs) - -Records are implicitly parameterized over a kind `u`, which stands for the -"universe" or key space. Keys (inhabitants of `u`) are then interpreted into -the types of their values by the first parameter to `Rec`, `f`. An extremely -powerful aspect of Vinyl records is that you can construct natural -transformations between different interpretation functors `f,g`, or postcompose -some other functor onto the stack. This can be used to immerse each field of a -record in some particular effect modality, and then the library functions can -be used to traverse and accumulate these effects. - -Let’s imagine that we want to do validation on a record that -represents a name and an age: - -> type Person = [Name, Age] - -We’ve decided that names must be alphabetic, and ages must be positive. For -validation, we’ll use `Maybe` for now, though you should use a -left-accumulating `Validation` type. - -> goodPerson :: Rec Attr Person -> goodPerson = (SName =:: "Jon") -> :& (SAge =:: 20) -> :& RNil - -> badPerson = (SName =:: "J#@#$on") -> :& (SAge =:: 20) -> :& RNil - -We'll give validation a (rather poor) shot. - -> validatePerson :: Rec Attr Person -> Maybe (Rec Attr Person) -> validatePerson p = (\n a -> (SName =:: n) :& (SAge =:: a) :& RNil) <$> vName <*> vAge where -> vName = validateName $ p ^. rlens @'Name . unAttr -> vAge = validateAge $ p ^. rlens @'Age . unAttr -> -> validateName str | all isAlpha str = Just str -> validateName _ = Nothing -> validateAge i | i >= 0 = Just i -> validateAge _ = Nothing - -> -- $setup -> -- >>> let isJust (Just _) = True; isJust _ = False - -> -- | -> -- >>> isJust $ validatePerson goodPerson -> -- True -> -- -> -- >>> isJust $ validatePerson badPerson -> -- False - -The results are as expected (`Just` for `goodPerson`, and a `Nothing` for -`badPerson`); but this was not very fun to build. - -Further, it would be nice to have some notion of a partial record; -that is, if part of it can’t be validated, it would still be nice to -be able to access the rest. What if we could make a version of this -record where the elements themselves were validation functions, and -then that record could be applied to a plain one, to get a record of -validated fields? That’s what we’re going to do. - -> type Validator f = Lift (->) f (Maybe :. f) - -Let’s parameterize a record by it: when we do, then an element of type -`a` should be a function `Identity a -> Result e a`: - -> vperson :: Rec (Validator Attr) Person -> vperson = lift validateName :& lift validateAge :& RNil -> where -> lift f = Lift $ Compose . f -> validateName (Attr str) | all isAlpha str = Just (Attr str) -> validateName _ = Nothing -> validateAge (Attr i) | i >= 0 = Just (Attr i) -> validateAge _ = Nothing - -And we can use the special application operator `<<*>>` (which is -analogous to `<*>`, but generalized a bit) to use this to validate a -record: - -> goodPersonResult = vperson <<*>> goodPerson -> badPersonResult = vperson <<*>> badPerson - -> -- | -> -- >>> :set -XTypeApplications -XDataKinds -> -- >>> isJust . getCompose $ goodPersonResult ^. rlens @Name -> -- True -> -- >>> isJust . getCompose $ goodPersonResult ^. rlens @Age -> -- True -> -- >>> isJust . getCompose $ badPersonResult ^. rlens @Name -> -- False -> -- >>> isJust . getCompose $ badPersonResult ^. rlens @Age -> -- True - - -So now we have a partial record, and we can still do stuff with its contents. -Next, we can even recover the original behavior of the validator (that is, to -give us a value of type `Maybe (Rec Attr Person)`) using `rtraverse`: - -> mgoodPerson :: Maybe (Rec Attr Person) -> mgoodPerson = rtraverse getCompose goodPersonResult - -> mbadPerson = rtraverse getCompose badPersonResult - -> -- | -> -- >>> isJust mgoodPerson -> -- True -> -- >>> isJust mbadPerson -> -- False - -> main :: IO () -> main = doctest ["tests/Intro.lhs", "Data/Vinyl/Tutorial/Overview.hs"] diff --git a/tests/doctests.hs b/tests/doctests.hs index 872a4ce..a5b5b94 100644 --- a/tests/doctests.hs +++ b/tests/doctests.hs @@ -1,14 +1,8 @@ -{-# language CPP #-} -import Test.DocTest +module Main where main :: IO () -main = doctest [ "-package lens" - , "-package doctest" -#if __GLASGOW_HASKELL__ >= 900 - , "-package singletons-th" -#else - , "-package singletons" -#endif - , "tests/Intro.lhs" - , "Data/Vinyl/Functor.hs" - , "Data/Vinyl/Curry.hs" ] +main = do + putStrLn "This test-suite exists only to add dependencies" + putStrLn "To run doctests: " + putStrLn " cabal build all --enable-tests" + putStrLn " cabal-docspec" diff --git a/vinyl.cabal b/vinyl.cabal index 5e6736c..65b7a2b 100644 --- a/vinyl.cabal +++ b/vinyl.cabal @@ -43,16 +43,15 @@ library build-depends: base >= 4.11 && <= 5, ghc-prim, deepseq, - array, - singletons + array if impl (ghc < 8.6.0) build-depends: constraints >= 0.6.1 - if impl (ghc < 9.0.1) - build-depends: singletons >= 0.10 && < 3 - else - build-depends: singletons-th >= 3 && < 3.1 default-language: Haskell2010 ghc-options: -Wall + if impl (ghc < 9.0.1) + x-docspec-extra-packages: lens, singletons + else + x-docspec-extra-packages: lens, singletons-th other-extensions: TypeApplications benchmark storable @@ -98,17 +97,17 @@ benchmark asa ghc-options: -O2 default-language: Haskell2010 --- TODO: Use cabal-docspec --- test-suite doctests --- type: exitcode-stdio-1.0 --- hs-source-dirs: tests --- other-modules: Intro --- main-is: doctests.hs --- if impl (ghc < 9.0.1) --- build-depends: base, lens, doctest >= 0.8, singletons >= 0.10 && < 3, vinyl --- else --- build-depends: base, lens, doctest >= 0.8, singletons-th >= 3 && < 3.1, vinyl --- default-language: Haskell2010 +-- Dummy test for cabal-docspec dependencies that are used in +-- Data.Vinyl.Tutorial.Overview +test-suite doctests + type: exitcode-stdio-1.0 + hs-source-dirs: tests + main-is: doctests.hs + if impl (ghc < 9.0.1) + build-depends: base, lens singletons >= 0.10 && < 3, vinyl + else + build-depends: base, lens singletons-th >= 3 && < 3.1, vinyl + default-language: Haskell2010 test-suite aeson type: exitcode-stdio-1.0 From 2d193dae2d5a1a141ae0b84c952dfe3257a8f938 Mon Sep 17 00:00:00 2001 From: Matthias Meschede Date: Sat, 28 Oct 2023 09:28:53 +0200 Subject: [PATCH 54/54] add cabal-plan to dev tools --- flake.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/flake.nix b/flake.nix index d11528b..3213aea 100644 --- a/flake.nix +++ b/flake.nix @@ -57,6 +57,7 @@ ghc hspkgs.cabal-install hspkgs.haskell-language-server + hspkgs.cabal-plan nurpkgs.repos.amesgen.cabal-docspec ]; };