cmptype (empty) → 0.1.0.0

raw patch · 11 files changed

+396/−0 lines, 11 filesdep +basedep +cmptypedep +ghcsetup-changed

Dependencies added: base, cmptype, ghc, magic-tyfams, should-not-typecheck

Files

• ChangeLog.md +7/−0
• LICENSE +30/−0
• README.md +37/−0
• Setup.hs +2/−0
• cmptype.cabal +60/−0
• src/GHC/NameViolation.hs +56/−0
• src/Type/Compare.hs +20/−0
• src/Type/Compare/Plugin.hs +37/−0
• test/Main.hs +9/−0
• test/ShouldNotTypecheck.hs +38/−0
• test/ShouldTypecheck.hs +100/−0

@@ -0,0 +1,7 @@+# Changelog for type-sets++## 0.1.0.0 --- 2019-08-05++Initial release!++## Unreleased changes

@@ -0,0 +1,30 @@+Copyright Sandy Maguire (c) 2019++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 Sandy Maguire 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.

@@ -0,0 +1,37 @@+# cmptype++[![Hackage](https://img.shields.io/hackage/v/cmptype.svg?logo=haskell&label=cmptype)](https://hackage.haskell.org/package/cmptype)++## Dedication++> Comparison is an act of violence against the self.+>+> --Iyanla Vanzant+++## Overview++`cmptype` provides a magical type family that lets you compare types:++```haskell+type family CmpType (a :: k) (b :: k) :: Ordering+```++When you turn on the `-fplugin=Type.Compare.Plugin` flag, it will let you+compare arbitrary types. Why would you want such a thing? Probably because you+want to write a [type-level container that isn't a fucking list][type-sets]!++[type-sets]: https://github.com/isovector/type-sets+++## Acknowledgments++Big thanks to [Boris Rozinov][oofp] for the initial idea, and for making as much+coffee as I could drink while I wrote it. Also thanks to [Christiaan+Baaij][chistiaanb] and [Matt Pickering][mpickering] for their indispensable help+convincing GHC to do the right thing here.++[oofp]: https://github.com/oofp+[chistiaanb]: https://christiaanb.github.io/+[mpickering]: http://mpickering.github.io/+

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,60 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 961cf4bb432f401123d81aa11c22e60aaab80702b2adb69c1bd87dcf6d8881c9++name:           cmptype+version:        0.1.0.0+synopsis:       Compare types of any kinds+description:    Please see the README on GitHub at <https://github.com/isovector/type-sets/tree/master/cmptype#readme>+category:       Type+homepage:       https://github.com/https://github.com/isovector/type-sets/tree/master/cmptype#readme+bug-reports:    https://github.com/https://github.com/isovector/type-sets/tree/master/cmptype/issues+author:         Sandy Maguire+maintainer:     sandy@sandymaguire.me+copyright:      2019 Sandy Maguire+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/https://github.com/isovector/type-sets/tree/master/cmptype++library+  exposed-modules:+      Type.Compare+      Type.Compare.Plugin+  other-modules:+      GHC.NameViolation+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , ghc >=8.6.3 && <8.8+    , magic-tyfams >=0.1.0.0 && <0.2+  default-language: Haskell2010++test-suite test+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      ShouldNotTypecheck+      ShouldTypecheck+      Paths_cmptype+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -fplugin=Type.Compare.Plugin+  build-depends:+      base >=4.7 && <5+    , cmptype+    , ghc >=8.6.3 && <8.8+    , magic-tyfams >=0.1.0.0 && <0.2+    , should-not-typecheck+  default-language: Haskell2010

@@ -0,0 +1,56 @@+module GHC.NameViolation where++import qualified Name as N+import FastString+import Unique+import SrcLoc+import Module+import TyCoRep+import Unsafe.Coerce+++violateName :: N.Name -> Name+violateName = unsafeCoerce+++showName :: Name -> String+showName (Name (External m) occ _ _)    =+  showModule m ++ "." ++ unpackFS (occNameFS occ)+showName (Name (WiredIn m _ _) occ _ _) =+  showModule m ++ "." ++ unpackFS (occNameFS occ)+showName (Name Internal occ _ _) =+  unpackFS (occNameFS occ)+showName (Name System occ _ _) =+  unpackFS (occNameFS occ)++++showModule :: Module -> String+showModule = moduleStableString+++data OccName = OccName+  { occNameSpace  :: !N.NameSpace+  , occNameFS     :: !FastString+  }+++data Name = Name+  { n_sort :: NameSort     -- What sort of name it is+  , n_occ  :: !OccName     -- Its occurrence name+  , n_uniq :: {-# UNPACK #-} !Unique+  , n_loc  :: !SrcSpan      -- Definition site+  }+++data NameSort+  = External Module++  | WiredIn Module TyThing N.BuiltInSyntax+        -- A variant of External, for wired-in things++  | Internal            -- A user-defined Id or TyVar+                        -- defined in the module being compiled++  | System              -- A system-defined Id or TyVar.  Typically the+                        -- OccName is very uninformative (like 's')

@@ -0,0 +1,20 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Compare where++import GHC.TypeLits++------------------------------------------------------------------------------+-- | Compare two types. For 'Nat's and 'Symbol's, this uses the built-in+-- comparisons. For all other types, "Type.Compare.Plugin" will solve it.+--+-- The actual /meaning/ of comparing types is left to your imagination. But it's+-- deterministic so that's good enough.+type family CmpType (a :: k) (b :: k) :: Ordering where+  CmpType a             a = 'EQ+  CmpType (a :: Nat)    b = CmpNat a b+  CmpType (a :: Symbol) b = CmpSymbol a b+

@@ -0,0 +1,37 @@+{-# LANGUAGE BangPatterns  #-}+{-# LANGUAGE LambdaCase    #-}+{-# LANGUAGE TupleSections #-}+{-# OPTIONS_GHC -Wall      #-}++module Type.Compare.Plugin (plugin) where++import Plugin.MagicTyFam (magicTyFamPlugin, isTyFamFree)+import Control.Applicative (liftA2)+import Control.Monad (guard)+import Data.List (intercalate)+import GHC.NameViolation (violateName, showName)+import GhcPlugins+++------------------------------------------------------------------------------+-- | This plugin automagically solves 'Type.Compare.CmpType'. Enable the GHC+-- flag @-fplugin=Type.Compare.Plugin@ in order to use it.+plugin :: Plugin+plugin = magicTyFamPlugin "cmptype" "Type.Compare" "CmpType" $ \[_, a, b] ->+  fmap promoteOrdering $ liftA2 compare (hash a) (hash b)+++promoteOrdering :: Ordering -> Type+promoteOrdering = flip mkTyConApp [] . \case+   LT -> promotedLTDataCon+   EQ -> promotedEQDataCon+   GT -> promotedGTDataCon+++hash :: Type -> Maybe String+hash t = do+  guard $ isTyFamFree t+  (c, as) <- splitTyConApp_maybe t+  hs <- traverse hash as+  pure $ intercalate " " $ showName (violateName $ getName c) : hs+

@@ -0,0 +1,9 @@+module Main where++import ShouldTypecheck ()+import ShouldNotTypecheck++main :: IO ()+main = testStuckInstances++

@@ -0,0 +1,38 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds      #-}+{-# LANGUAGE TypeFamilies   #-}+{-# LANGUAGE TypeOperators  #-}++{-# OPTIONS_GHC -fdefer-type-errors+                -fno-warn-deferred-type-errors+                #-}++-- TODO(sandy): It would be nice to have a better way of observing stuckness.+module ShouldNotTypecheck where++import Data.Proxy+import GHC.TypeLits+import Test.ShouldNotTypecheck+import Type.Compare+++type family Stuck :: k++testWrongType1 :: Proxy (CmpType a b) -> Proxy 'LT+testWrongType1 = id++testWrongType2 :: Proxy (CmpType Stuck Int) -> Proxy 'GT+testWrongType2 = id++testWrongType3 :: Proxy (CmpType (0 - 1) 2) -> Proxy 'GT+testWrongType3 = id+++testStuckInstances :: IO ()+testStuckInstances = do+  shouldNotTypecheck testWrongType1+  shouldNotTypecheck testWrongType2+  shouldNotTypecheck testWrongType3++

@@ -0,0 +1,100 @@+{-# LANGUAGE DataKinds      #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies   #-}++{-# OPTIONS_GHC -fplugin=Type.Compare.Plugin   #-}++module ShouldTypecheck where++import           Data.Proxy+import           GHC.TypeLits+import qualified Prelude as P+import           Prelude hiding (Int)+import           Type.Compare+++testSym1 :: Proxy (CmpType "a" "apple") -> Proxy 'LT+testSym1 = id++testSym2 :: Proxy (CmpType "banana" "banana") -> Proxy 'EQ+testSym2 = id++testSym3 :: Proxy (CmpType "dominos" "cabana") -> Proxy 'GT+testSym3 = id+++testNat1 :: Proxy (CmpType 0 1) -> Proxy 'LT+testNat1 = id++testNat2 :: Proxy (CmpType 2 2) -> Proxy 'EQ+testNat2 = id++testNat3 :: Proxy (CmpType 4 3) -> Proxy 'GT+testNat3 = id+++data Apricot+data Blueberry+data Coconut+data Durian++testType1 :: Proxy (CmpType Apricot Blueberry) -> Proxy 'LT+testType1 = id++testType2 :: Proxy (CmpType Coconut Coconut) -> Proxy 'EQ+testType2 = id++testType3 :: Proxy (CmpType Durian Coconut) -> Proxy 'GT+testType3 = id+++type family IsEQ (ord :: Ordering) :: Bool where+  IsEQ 'EQ = 'True+  IsEQ _   = 'False++testType4 :: Proxy (IsEQ (CmpType Durian Coconut)) -> Proxy 'False+testType4 = id++testType5 :: Proxy (IsEQ (CmpType Blueberry Blueberry)) -> Proxy 'True+testType5 = id++testType6 :: Proxy (CmpType [Apricot] [Blueberry]) -> Proxy 'LT+testType6 = id++testType7 :: Proxy (CmpType [Durian] [Coconut]) -> Proxy 'GT+testType7 = id++testType8 :: Proxy '[CmpType [Durian] [Coconut]] -> Proxy '[ 'GT ]+testType8 = id++testType9 :: Proxy '[IsEQ (CmpType [Durian] [Coconut])] -> Proxy '[ 'False ]+testType9 = id++testType10 :: Proxy '[IsEQ (CmpType [[Apricot]] [[Apricot]])] -> Proxy '[ 'True ]+testType10 = id++testType11 :: Proxy '[IsEQ (CmpType [Apricot] [[Apricot]])] -> Proxy '[ 'False ]+testType11 = id+++data Int++testType12 :: Proxy (IsEQ (CmpType Int P.Int)) -> Proxy 'False+testType12 = id++testType13 :: Proxy (IsEQ (CmpType '[Int] '[P.Int])) -> Proxy 'False+testType13 = id++testType14 :: Proxy (CmpType '(Int, Int) '(Int, Bool)) -> Proxy 'GT+testType14 = id++testType15 :: Proxy (CmpType '[Int, Bool] '[Int, Bool]) -> Proxy 'EQ+testType15 = id++testType16 :: Proxy (CmpType '[Int, Int] '[Int, Bool]) -> Proxy 'GT+testType16 = id++-- NOTE(sandy): I don't really understand why this one is so...+testType17 :: Proxy (CmpType '[Int, Bool] '[]) -> Proxy 'LT+testType17 = id+