singlethongs (empty) → 0.1

raw patch · 8 files changed

+358/−0 lines, 8 filesdep +basedep +singlethongsdep +template-haskell

Dependencies added: base, singlethongs, template-haskell

Files

CHANGELOG.md +5/−0
LICENSE +33/−0
README.md +14/−0
lib/Singlethongs.hs +39/−0
lib/Singlethongs/Internal.hs +25/−0
lib/Singlethongs/TH.hs +124/−0
singlethongs.cabal +42/−0
test/Main.hs +76/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# 0.1++* Initial version, more or less based on `singletons-2.5.1`.++* Builds with GHC 8.6.5, GHC 8.8.2, GHCJS 8.6.0.

+ LICENSE view

@@ -0,0 +1,33 @@+Copyright (c) 2020, Renzo Carbonara. All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+list of conditions and the following disclaimer.++2. 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.++3. Neither the name of the author nor the names of its 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 HOLDER 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.++--++This project is based on "singletons", Copyright (c) 2012 Richard+Eisenberg, licenced under the terms of the BSD-3-Clause license at+https://hackage.haskell.org/package/singletons-2.5.1/src/LICENSE+

+ README.md view

@@ -0,0 +1,14 @@+# Singlethongs++Like [singletons](https://hackage.haskell.org/package/singletons), but much+smaller.++# Development++* Build all with `nix-build`.++* Build with some GHC or GHCJS version with `nix-build -A $xxx`, where `xxx` is+  one of `ghc865`, `ghc882`, `ghcjs86`.++* Enter a development environment with `nix-shell -A $xxx.env`, where `xxx` is+  one of `ghc865`, `ghc882`, `ghcjs86`.

+ lib/Singlethongs.hs view

@@ -0,0 +1,39 @@+{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}++{- | The goal of+the [singlethongs](https://hackage.haskell.org/package/singlethongs) library+is to offer the bare minimum of what+the [singletons](https://hackage.haskell.org/package/singletons) library offers+in a small package that's easy to compile across different GHC versions,+including GHCJS.++This module exports a minimal reproduction of what+the [singletons](https://hackage.haskell.org/package/singletons) package offers.+Namely 'Sing', 'SingI', 'SomeSing' and 'SingKind', as well as @TemplateHaskell@+support for generating the relevant instances for custom types. If there is+some feature that you thing could be added to this library,+please [suggest it](https://gitlab.com/k0001/singlethongs/issues).++The types exported by this module are not the same types as the types as the+one exported by+the [singletons](https://hackage.haskell.org/package/singletons) package.+Even if they have the same names and implementation, they are not seen as+equal by the type-checker. They are only intended to be a drop-in replacement.+-}+module Singlethongs+ ( Sing+ , SingI(..)+ , SomeSing(..)+ , withSomeSing+ , SingKind(..)+   -- * Template Haskell+ , singlethongs+   -- * Re-exports+ , TestEquality(testEquality)+ , (:~:)(Refl)+ ) where++import Singlethongs.Internal+import Singlethongs.TH+import Data.Type.Equality+

+ lib/Singlethongs/Internal.hs view

@@ -0,0 +1,25 @@+{-# LANGUAGE GADTs, KindSignatures, PolyKinds, TypeFamilies, RankNTypes #-}+module Singlethongs.Internal+ ( Sing+ , SingI(sing)+ , SomeSing(SomeSing)+ , withSomeSing+ , SingKind(Demote, fromSing, toSing)+ ) where++data family Sing (a :: k)++class SingI (a :: k) where+  sing :: Sing a++data SomeSing k where+  SomeSing :: Sing (a :: k) -> SomeSing k++withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r+withSomeSing x f = case toSing x of SomeSing x' -> f x'+{-# INLINE withSomeSing #-}++class SingKind k where+  type Demote k :: *+  fromSing :: Sing (a :: k) -> Demote k+  toSing :: Demote k -> SomeSing k

+ lib/Singlethongs/TH.hs view

@@ -0,0 +1,124 @@+{-# LANGUAGE CPP, LambdaCase, TemplateHaskell #-}+module Singlethongs.TH (singlethongs) where++import Data.Type.Equality+import Language.Haskell.TH+import Singlethongs.Internal++{-| Generate 'Sing', 'SingI', 'SingKind' and 'TestEquality' instances for a+datatype.++Given a datatype like @Foo@ below, having one or more unary constructors:++@+data Foo = Bar | Qux++'singlethongs' ''Foo+@++The following code will be generated:++@+data instance 'Sing' (x :: Foo) where+  SBar :: 'Sing' 'Bar+  SQux :: 'Sing' 'Qux++instance 'SingKind' Fobo where+  type 'Demote' Foo = Foo+  'fromSing' SBar = Bar+  'fromSing' SQux = Qux+  'toSing' Bar = 'SomeSing' SBar+  'toSing' Qux = 'SomeSing' SQux++instance 'SingI' 'Bar where 'sing' = SBar+instance 'SingI' 'Qux where 'sing' = SQux++instance 'TestEquality' ('Sing' :: Foo -> *) where+  'testEquality' SBar SBar = 'Just' 'Refl'+  'testEquality' SQux SQux = 'Just' 'Refl'+  'testEquality' _ _ = 'Nothing'+@++In order to use this 'singlethongs' function, you will need to enable the+following GHC extensions:++@+\{\-\# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies \#\-\}+@+-}++singlethongs :: Name -> Q [Dec]+singlethongs n0 = reify n0 >>= \case+  TyConI (DataD [] n1 [] Nothing cons@(_:_) []) -> do+    nCons <- traverse conName cons+    out0 <- genDataInstSing n1 nCons+    out1 <- genInstanceSingKind n1 nCons+    out2 <- genInstanceTestEquality n1 nCons+    out3 <- mconcat <$> traverse genInstanceSingI nCons+    pure (out0 <> out1 <> out2 <> out3)+  _ -> fail "Only enum types are acceptable"++conName :: Con -> Q Name+conName = \case+  NormalC n [] -> pure n+  _ -> fail "Only enum types are acceptable"++sName :: Name -> Name+sName a = mkName ("S" <> nameBase a)++genDataInstSing :: Name -> [Name] -> Q [Dec]+genDataInstSing nTy nCons = do+  let cons1 = flip fmap nCons $ \nCon ->+        GadtC [sName nCon] [] (AppT (ConT ''Sing) (PromotedT nCon))+  pure [mkSingDataInstD nTy cons1]++genInstanceSingI :: Name -> Q [Dec]+genInstanceSingI nCon = do+  let singD = FunD (mkName "sing") [Clause [] (NormalB (ConE (sName nCon))) []]+  pure [InstanceD Nothing [] (AppT (ConT ''SingI) (PromotedT nCon)) [singD]]++genInstanceSingKind :: Name -> [Name] -> Q [Dec]+genInstanceSingKind nTy nCons = do+  let fromSingD = FunD (mkName "fromSing") $ flip fmap nCons $ \nCon ->+        Clause [ConP (sName nCon) []] (NormalB (ConE nCon)) []+      toSingD = FunD (mkName "toSing") $ flip fmap nCons $ \nCon ->+        Clause [ConP nCon []]+               (NormalB (AppE (ConE 'SomeSing) (ConE (sName nCon)))) []+  pure [InstanceD Nothing [] (AppT (ConT ''SingKind) (ConT nTy))+         [mkDemoteD nTy, fromSingD, toSingD] ]++genInstanceTestEquality :: Name -> [Name] -> Q [Dec]+genInstanceTestEquality nTy nCons = do+  let teD = FunD (mkName "testEquality") $ mconcat+       [ flip fmap nCons $ \nCon ->+           let p = ConP (sName nCon) []+           in Clause [p, p] (NormalB (AppE (ConE 'Just) (ConE 'Refl))) []+       , case nCons of+           [_] -> []+           _ -> [Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []]+       ]+  pure [InstanceD Nothing []+          (AppT (ConT ''TestEquality)+                (SigT (ConT ''Sing)+                      (AppT (AppT ArrowT (ConT nTy)) StarT)))+          [teD ]]+++mkDemoteD :: Name -> Dec+mkDemoteD nTy =+#if MIN_VERSION_template_haskell(2,15,0)+  TySynInstD (TySynEqn Nothing (AppT (ConT ''Demote) (ConT nTy)) (ConT nTy))+#else+  TySynInstD ''Demote (TySynEqn [ConT nTy] (ConT nTy))+#endif++mkSingDataInstD :: Name -> [Con] -> Dec+mkSingDataInstD nTy cons =+#if MIN_VERSION_template_haskell(2,15,0)+  DataInstD [] Nothing (AppT (ConT ''Sing) (SigT (VarT (mkName "x")) (ConT nTy)))+            Nothing cons []+#else+  DataInstD [] ''Sing [SigT (VarT (mkName "x")) (ConT nTy)] Nothing cons []+#endif++

+ singlethongs.cabal view

@@ -0,0 +1,42 @@+cabal-version: 2.4+name: singlethongs+version: 0.1+license: BSD-3-Clause+license-file: LICENSE+extra-source-files:  README.md CHANGELOG.md+author: Renzo Carbonara+maintainer: renλren.zone+copyright: Copyright (c) Renzo Carbonara 2020+category: Data+build-type: Simple+synopsis: Like singletons, but much smaller.+description: Like singletons, but much smaller.+homepage: https://gitlab.com/k0001/singlethongs+bug-reports: https://gitlab.com/k0001/singlethongs/issues+tested-with:+  GHC == 8.6.0,+  GHC == 8.6.5,+  GHC == 8.8.2++library+  hs-source-dirs: lib+  ghc-options: -Wall -Werror=incomplete-patterns -O2+  ghcjs-options: -Wall -Werror=incomplete-patterns -O3+  default-language: Haskell2010+  exposed-modules:+    Singlethongs+  other-modules:+    Singlethongs.Internal+    Singlethongs.TH+  build-depends:+    base ==4.*,+    template-haskell,++test-suite test+  default-language: Haskell2010+  type: exitcode-stdio-1.0+  hs-source-dirs: test+  main-is: Main.hs+  build-depends:+    base,+    singlethongs,

+ test/Main.hs view

@@ -0,0 +1,76 @@+{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies,+             ScopedTypeVariables, TypeApplications #-}+{-# OPTIONS_GHC -ddump-splices #-}++module Main (main) where++import Control.Monad (when)++-- We import qualified to test that TH names don't make silly assumptions.+import qualified Singlethongs as S+++data A = Ax deriving (Eq)+S.singlethongs ''A+{- =====>+data instance S.Sing (x :: A) where+  SAx :: S.Sing 'Ax++instance S.SingKind A where+  type S.Demote A = A+  fromSing SAx = Ax+  toSing Ax = S.SomeSing SAx++instance S.TestEquality (S.Sing :: A -> *) where+  testEquality SAx SAx = Just S.Refl++instance S.SingI 'Ax where sing = SAx+-}++t_A :: Bool+t_A = and+  [ S.fromSing (SAx :: S.Sing 'Ax) == (Ax :: S.Demote A)+  , S.withSomeSing @A Ax (\sAx -> S.fromSing sAx == Ax)+  , S.testEquality SAx SAx == Just S.Refl+  ]++data B = Bx | By deriving (Eq)+S.singlethongs ''B+{- =====>++data instance S.Sing (x :: B) where+  SBx :: S.Sing 'Bx+  SBy :: S.Sing 'By++instance S.SingKind B where+  type S.Demote B = B+  fromSing SBx = Bx+  fromSing SBy = By+  toSing Bx = S.SomeSing SBx+  toSing By = S.SomeSing SBy++instance S.TestEquality (S.Sing :: B -> *) where+  testEquality SBx SBx = Just S.Refl+  testEquality SBy SBy = Just S.Refl+  testEquality _ _ = Nothing++instance S.SingI  'Bx where sing = SBx+instance S.SingI  'By where sing = SBy+-}++t_B :: Bool+t_B = and+  [ S.fromSing (SBx :: S.Sing 'Bx) == (Bx :: S.Demote B)+  , S.withSomeSing @B Bx (\sBx -> S.fromSing sBx == Bx)+  , S.fromSing (SBy :: S.Sing 'By) == (By :: S.Demote B)+  , S.withSomeSing @B By (\sBy -> S.fromSing sBy == By)+  , S.testEquality SBx SBx == Just S.Refl+  , S.testEquality SBx SBy == Nothing+  , S.testEquality SBy SBx == Nothing+  , S.testEquality SBy SBy == Just S.Refl+  ]++main :: IO ()+main = do+  when (not t_A) $ fail "Something wrong with t_A"+  when (not t_B) $ fail "Something wrong with t_B"