diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for closed-classes + +## 0.1.0.0 -- 2021-09-08 + +* Initial version. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2021, Anthony Vandikas + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Anthony Vandikas nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/closed-classes.cabal b/closed-classes.cabal new file mode 100644 --- /dev/null +++ b/closed-classes.cabal @@ -0,0 +1,39 @@ +cabal-version: 2.4 +name: closed-classes +version: 0.1 +synopsis: Closed type class declarations +description: See "Data.Class.Closed" for explanation. +homepage: https://github.com/YellPika/closed-classes +bug-reports: https://github.com/YellPika/closed-classes/issues +license: BSD-3-Clause +license-file: LICENSE +author: Anthony Vandikas +maintainer: yellpika@gmail.com +copyright: © 2021 Anthony Vandikas +category: Type System +extra-source-files: CHANGELOG.md + +library + exposed-modules: Data.Class.Closed + Data.Class.Closed.Example + Data.Class.Closed.TH + other-extensions: CPP + DataKinds + DefaultSignatures + FlexibleContexts + FlexibleInstances + KindSignatures + MonoLocalBinds + MultiParamTypeClasses + PolyKinds + TemplateHaskell + TypeApplications + TypeOperators + UndecidableInstances + UnicodeSyntax + ViewPatterns + build-depends: base >=4.14 && <4.17, + template-haskell >=2.16 && <2.19 + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall diff --git a/src/Data/Class/Closed.hs b/src/Data/Class/Closed.hs new file mode 100644 --- /dev/null +++ b/src/Data/Class/Closed.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE UnicodeSyntax #-} + +-- | Closed type classes are defined by adding a private field with a default +-- implementation that requires a 'Closed' constraint. For example: +-- +-- > {-# LANGUAGE DefaultSignatures, FlexibleContexts #-} +-- > +-- > module Foo (Foo) where +-- > +-- > class Foo a where +-- > default _private :: Closed Foo => Proxy a +-- > _private :: Proxy a +-- > _private = Proxy +-- > +-- > instance Foo Int where +-- > _private = Proxy +-- +-- Since @_private@ is not exported, any new instance defined outside the @Foo@ +-- module will be forced to use the default implementation, which has the +-- unsatisfiable 'Closed' @Foo@ constraint. +-- +-- > module Bar where +-- > +-- > import Foo +-- > +-- > instance Foo Char -- • User defined Foo instances are not allowed. +-- +-- Thus new instances can only be defined in the same module as @Foo@, where +-- @_private@ is visible. Note that 'Closed' itself is a closed type class, +-- implemented using the same trick! +-- +-- To automatically generate the boilerplate, see "Data.Class.Closed.TH". +module Data.Class.Closed (Closed) where + +import Data.Proxy (Proxy (..)) +import GHC.TypeLits (ErrorMessage (..), TypeError) + +-- | 'Closed' constraints are unsatisfiable. Attempting to resolve a 'Closed' +-- @\@ constraint will result in +-- +-- > • User defined instances are not allowed. +class Closed (a ∷ k) where + default _private ∷ Closed (Closed @k) ⇒ Proxy a + _private ∷ Proxy a + _private = Proxy + +instance TypeError ('Text "User defined " ':<>: 'ShowType a ':<>: 'Text " instances are not allowed.") ⇒ Closed a where + _private = Proxy diff --git a/src/Data/Class/Closed/Example.hs b/src/Data/Class/Closed/Example.hs new file mode 100644 --- /dev/null +++ b/src/Data/Class/Closed/Example.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE UnicodeSyntax #-} + +module Data.Class.Closed.Example ( + -- Explicit export is required or else the private field will be exported. + Example₁ (example₁), + Example₂ (example₂) +) where + +import Data.Class.Closed.TH (close) +import Data.Proxy (Proxy (..)) + +close [d| + class Example₁ a where + example₁ ∷ a + instance Example₁ () where + example₁ = () + class Example₂ a b where + example₂ ∷ a → Proxy (b ∷ Bool) + instance Example₂ a 'True where + example₂ _ = Proxy + |] + +-- The following does not work unless it is moved inside the quotation. +-- instance Example₁ Int where +-- example₁ = 0 diff --git a/src/Data/Class/Closed/TH.hs b/src/Data/Class/Closed/TH.hs new file mode 100644 --- /dev/null +++ b/src/Data/Class/Closed/TH.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE ViewPatterns #-} + +module Data.Class.Closed.TH where + +import Data.Class.Closed (Closed) +import Data.Maybe (fromMaybe) +import Data.Proxy (Proxy (..)) +import Language.Haskell.TH (Dec (..), Name, Q, TyVarBndr (..), Type (..), + appT, classD, clause, conT, defaultSigD, + funD, instanceWithOverlapD, nameBase, + newName, normalB, sigD, varT) +import Language.Haskell.TH.Syntax (getQ, putQ) + +-- | Closes all declared classes. Any instances must be given in the same quote. +close ∷ Q [Dec] -> Q [Dec] +close = (>>= mapM modify) where + modify ∷ Dec → Q Dec + modify (ClassD context name tvs deps decs) = do + let con = conT name + ty = foldl (\t b → appT t (binderT b)) con tvs + private ← getPrivateName name + classD (pure context) name tvs deps -- class ... ⇒ C ... where + $ defaultSigD private [t|Closed $con ⇒ Proxy $ty|] -- default private ∷ Closed C ⇒ Proxy (C ...) + : sigD private [t|Proxy $ty|] -- private ∷ Proxy (C ...) + : funD private [clause [] (normalB [|Proxy|]) []] -- private = Proxy + : map pure decs -- ... + modify (InstanceD overlap context ty@(conName → Just name) decs) = do + private ← getPrivateName name + instanceWithOverlapD overlap (pure context) (pure ty) -- instance ... where + $ funD private [clause [] (normalB [|Proxy|]) []] -- private = Proxy + : map pure decs -- ... + modify dec = pure dec + +#if MIN_VERSION_template_haskell(2, 17, 0) + binderT ∷ TyVarBndr flag → Q Type + binderT (PlainTV name _) = varT name + binderT (KindedTV name _ _) = varT name +#else + binderT ∷ TyVarBndr → Q Type + binderT (PlainTV name) = varT name + binderT (KindedTV name _) = varT name +#endif + + getPrivateName ∷ Name → Q Name + getPrivateName name = do + cache ← fromMaybe [] <$> getQ + case lookup name cache of + Just private → return private + Nothing → do + temp ← newName ("_" ++ nameBase name) + private ← newName (show temp) + putQ ((name, private):cache) + return private + + conName ∷ Type → Maybe Name + conName (ConT n) = Just n + conName (AppT x _) = conName x + conName (AppKindT x _) = conName x + conName (SigT x _) = conName x + conName (InfixT _ n _) = Just n + conName (UInfixT _ n _) = Just n + conName (ParensT x) = conName x + conName _ = Nothing