diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,31 @@ +Original work Copyright (c) 2016, Allele Dev +Modified work Copyright (c) 2016, Patrick Thomson and Josh Vera + +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 Allele Dev 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/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,13 @@ +# fastsum + +This package provides `Data.Sum`, an open-union type, similar to the `Union` type that powers the implementation of [Oleg Kiselyov's extensible-effects library](http://okmij.org/ftp/Haskell/extensible/). + +Unlike most open-union implementations, this type is very fast to compile, even when the type-level list of alternatives contains hundreds of entries. Membership queries are constant-time, compiling to a single type-level natural lookup in a closed type family, unlike the traditional encoding of `Union`, which relies on recursive typeclass lookups. As such, this type lends itself to representing abstract syntax trees or other rich data structures. + +GHC 8's support for custom type errors provides readable type errors should membership constraints not be satisfied. + +In order to achieve speed, this package makes fewer guarantees about what can be proven given a `Member` instance. If you require a richer vocabulary to describe the implications of membership, you should use the traditional implementation of open-unions. + +# Credits + +This library is built on the work of Oleg Kiselyov, which was then modified by Allele Dev. It was extracted from Josh Vera's [effects](https://github.com/joshvera/effects/) library. Rob Rix implemented the `ElemIndex` type family and the `Apply` typeclass. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Main.hs b/examples/Main.hs new file mode 100644 --- /dev/null +++ b/examples/Main.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE DataKinds, DeriveFunctor, FlexibleContexts, KindSignatures, RankNTypes, TypeApplications, TypeOperators, UndecidableInstances #-} + +module Main where + +import Data.Monoid hiding (Sum(..)) +import Data.Sum + +-- okay, let's use Data.Sum to solve the expression problem +-- we'll build a little expression language, define an F-algebra, and print it out +-- you don't _have_ to use recursion schemes with Data.Sum, but they sure are nice + +-- standard fixed point of a Functor. in the real world we would use an actual +-- recursion schemes library, but who has time for that? +newtype Fix f = In { out :: f (Fix f) } + +-- here's our expression type - note that l is a type-level list of functors +type Expr (l :: [* -> *]) = Fix (Sum l) + +-- numbers +newtype Lit a = Lit Int deriving Functor + +-- smart constructor. the :< is pronounced "member": +-- what this says is that as long as Lit is a member of the type-level +-- list 'fs', we can inj it into an Expr that contains 'fs' +-- if we tried to inj it into an 'Expr [Thing1, Thing2]', +-- we would get an error message that Lit cannot be found in [Thing1, Thing2] +lit :: (Lit :< fs) => Int -> Expr fs +lit = In . inject . Lit + +-- parens +newtype Paren a = Paren a + deriving Functor + +paren :: (Paren :< fs) => Expr fs -> Expr fs +paren = In . inject . Paren + +-- math +data Op a + = Add a a + | Sub a a + | Mul a a + deriving Functor + +(+:), (-:), (*:) :: (Op :< fs) => Expr fs -> Expr fs -> Expr fs +a +: b = In (inject (Add a b)) +a -: b = In (inject (Sub a b)) +a *: b = In (inject (Mul a b)) + +infixl 6 +: +infixl 6 -: +infixl 7 *: + +-- here's our F-algebra that converts a sum type to a string +class Functor f => Pretty f where + pretty :: f String -> String + +instance Pretty Lit where + pretty (Lit i) = show i + +instance Pretty Paren where + pretty (Paren a) = "(" <> a <> ")" + +instance Pretty Op where + pretty (Add a b) = concat [a, " + ", b] + pretty (Sub a b) = concat [a, " - ", b] + pretty (Mul a b) = concat [a, " * ", b] + +-- this tells the compiler that any Sum type whose components +-- all implement Functor and Pretty supports pretty-printing too +instance (Apply Functor fs, Apply Pretty fs) => Pretty (Sum fs) where + pretty = apply @Pretty pretty + +-- a neutered catamorphism +runPretty :: Pretty f => Fix f -> String +runPretty = pretty . fmap runPretty . out + +example :: Expr '[Lit, Op, Paren] +example = paren (lit 5 +: lit 10) *: lit 2 + +main :: IO () +main = putStrLn (runPretty example) + +-- now, if you so desired, you could add a new data type: +-- > data Div a = Div a a +-- declare a Pretty instance for it, and then create a new value of type +-- > Expr '[Lit, Op, Paren, Div] +-- and you get a perfect solution to the expression problem: seamless extension of functionality and of data-types diff --git a/fastsum.cabal b/fastsum.cabal new file mode 100644 --- /dev/null +++ b/fastsum.cabal @@ -0,0 +1,52 @@ +name: fastsum +version: 0.1.0.0 +synopsis: A fast open-union type suitable for 100+ contained alternatives +homepage: https://github.com/patrickt/fastsum#readme +license: BSD3 +license-file: LICENSE +author: Rob Rix, Josh Vera, Allele Dev, Patrick Thomson +maintainer: patrickt@github.com +copyright: Rob Rix, Josh Vera, Allele Dev, Patrick Thomson 2016-2018 +category: Data +build-type: Simple +extra-source-files: README.md +cabal-version: >=1.10 +tested-with: GHC == 8.2.2 +description: + This package provides Data.Sum, an open-union type, similar to the Union type + that powers the implementation of Oleg Kiselyov's extensible-effects library. + . + Unlike most open-union implementations, this type is very fast to compile, + even when the type-level list of alternatives contains hundreds of entries. + Membership queries are constant-time, compiling to a single type-level natural + lookup in a closed type family, unlike the traditional encoding of Union, + which relies on recursive typeclass lookups. As such, this type lends itself + to representing abstract syntax trees or other rich data structures. + . + This project is safe to use in production. Any performance problems at + compile-time or runtime should be filed as bugs. + +flag build-examples + default: False + +library + hs-source-dirs: src + exposed-modules: Data.Sum + other-modules: Data.Sum.Templates + build-depends: base >= 4.7 && < 5 + , ghc-prim + , hashable + , template-haskell + default-language: Haskell2010 + +executable example + hs-source-dirs: examples + main-is: Main.hs + build-depends: base, fastsum + default-language: Haskell2010 + if !flag(build-examples) + buildable: False + +source-repository head + type: git + location: https://github.com/patrickt/fastsum diff --git a/src/Data/Sum.hs b/src/Data/Sum.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sum.hs @@ -0,0 +1,235 @@ +{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ConstraintKinds, DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_HADDOCK prune, ignore-exports #-} + +{-| +Module : Data.Sum +Description : Open sums (type-indexed co-products) for extensible effects. +Copyright : Allele Dev 2015 +License : BSD-3 +Maintainer : allele.dev@gmail.com +Stability : experimental +Portability : POSIX + +All operations are constant-time, and there is no Typeable constraint. + +This is a variation of Kiselyov's OpenUnion5.hs, which relies on +overlapping instances instead of closed type families. Closed type +families have their problems: overlapping instances can resolve even +for unground types, but closed type families are subject to a strict +apartness condition. +-} + +module Data.Sum + ( -- * The fundamental sum-of-products type + Sum + -- * Creating and extracting sums from products + , inject + , project + -- * Operating on sums' effects lists + , decompose + , decomposeLast + , weaken + -- * Membership prodicates + , Element + , type(:<) + , Elements + , type(:<:) + , ElemIndex + -- * Typeclass application. + , Apply(..) + , apply' + , apply2 + ) where + +import Data.Functor.Classes (Eq1(..), eq1, Ord1(..), compare1, Show1(..), showsPrec1) +import Data.Hashable (Hashable(..)) +import Data.Hashable.Lifted (Hashable1(..), hashWithSalt1) +import Data.Maybe (fromMaybe) +import Data.Sum.Templates +import GHC.Exts (Constraint) +import GHC.Prim (Proxy#, proxy#) +import GHC.TypeLits +import Unsafe.Coerce(unsafeCoerce) + +pure [mkElemIndexTypeFamily 150] + +infixr 5 :< + +-- | The fundamental sum type over a type-level list of products @r@ +-- and an annotation type @v@. The constructor is not exported; +-- use 'inject' to create a 'Sum'. +data Sum (r :: [ * -> * ]) (v :: *) where + -- | Strong Sum (Existential with the evidence) is an open sum + -- t is can be a GADT and hence not necessarily a Functor. + -- Int is the index of t in the list r; that is, the index of t in the + -- universe r. + Sum :: {-# UNPACK #-} !Int -> t v -> Sum r v + +unsafeInject :: Int -> t v -> Sum r v +unsafeInject = Sum +{-# INLINE unsafeInject #-} + +unsafeProject :: Int -> Sum r v -> Maybe (t v) +unsafeProject n (Sum n' x) | n == n' = Just (unsafeCoerce x) + | otherwise = Nothing +{-# INLINE unsafeProject #-} + +newtype P (t :: * -> *) (r :: [* -> *]) = P { unP :: Int } + +infixr 5 :<: +-- | An @Elements ms r@ constraint proves that @r@ contains +-- all of the elements in @ms@. +type family Elements (ms :: [* -> *]) r :: Constraint where + Elements (t ': cs) r = (Element t r, Elements cs r) + Elements '[] r = () + +-- | An infix synonym for 'Elements'. +type (ts :<: r) = Elements ts r + +-- | Inject a functor into a type-aligned sum. +inject :: forall e r v. (e :< r) => e v -> Sum r v +inject = unsafeInject (unP (elemNo :: P e r)) +{-# INLINE inject #-} + +-- | Maybe project a functor out of a type-aligned sum. +project :: forall e r v. (e :< r) => Sum r v -> Maybe (e v) +project = unsafeProject (unP (elemNo :: P e r)) +{-# INLINE project #-} + +-- | Attempts to extract the head type @e@ from a @Sum@. Returns +-- @Right@ on success, and a @Sum@ without @e@ otherwise. You can +-- repeatedly apply this and apply 'decomposeLast' when you have @Sum +-- '[e]@ to get typesafe, exhaustive matching of an open sum. See +-- @examples/Errors.hs@ for a full example. +decompose :: Sum (e ': es) b -> Either (Sum es b) (e b) +decompose sum@(Sum n v) = maybe (Left (Sum (n - 1) v)) Right (project sum) +{-# INLINE decompose #-} + +-- | Special case of 'decompose' which knows that there is only one +-- possible type remaining in the @Sum@, @e@ thus it is guaranteed to +-- return @e@ +decomposeLast :: Sum '[e] b -> e b +decomposeLast = either (error "Data.Sum: impossible case in decomposeLast") id . decompose +{-# INLINE decomposeLast #-} + +-- | Add an arbitrary product @any@ to a product list @r@. +weaken :: Sum r w -> Sum (any ': r) w +weaken (Sum n v) = Sum (n+1) v + +-- | @Element t r@ is a proof that @t@ is a member of @r@. This is implemented +-- in terms of @KnownNat@ rather than recursive typeclass lookups. +type (Element t r) = KnownNat (ElemIndex t r) + +-- | An infix version of 'Element'. Note that you will need @-XTypeOperators@ +-- turned on to use this. +type (t :< r) = Element t r + +-- Find an index of an element in an `r'. +-- The element must exist, so this is essentially a compile-time computation. +elemNo :: forall t r . (t :< r) => P t r +elemNo = P (fromIntegral (natVal' (proxy# :: Proxy# (ElemIndex t r)))) + +-- | Helper to apply a function to a functor of the nth type in a type list. +-- An @Apply SomeClass fs@ instance means that @Sum fs@ has an instance of @SomeClass@. +-- Instances are written using 'apply' and an explicit type application: +-- +-- > instance Apply SomeClass fs => SomeClass (Sum fs) where method = apply @SomeClass method +-- +-- An @INLINEABLE@ pragma on such an instance may improve dispatch speed. +class Apply (c :: (* -> *) -> Constraint) (fs :: [* -> *]) where + apply :: (forall g . c g => g a -> b) -> Sum fs a -> b + +apply' :: forall c fs a b . Apply c fs => (forall g . c g => (forall x. g x -> Sum fs x) -> g a -> b) -> Sum fs a -> b +apply' f u@(Sum n _) = apply @c (f (Sum n)) u +{-# INLINABLE apply' #-} + +apply2 :: forall c fs a b d . Apply c fs => (forall g . c g => g a -> g b -> d) -> Sum fs a -> Sum fs b -> Maybe d +apply2 f u@(Sum n1 _) (Sum n2 r2) + | n1 == n2 = Just (apply @c (\ r1 -> f r1 (unsafeCoerce r2)) u) + | otherwise = Nothing +{-# INLINABLE apply2 #-} + +apply2' :: forall c fs a b d . Apply c fs => (forall g . c g => (forall x. g x -> Sum fs x) -> g a -> g b -> d) -> Sum fs a -> Sum fs b -> Maybe d +apply2' f u@(Sum n1 _) (Sum n2 r2) + | n1 == n2 = Just (apply' @c (\ reinject r1 -> f reinject r1 (unsafeCoerce r2)) u) + | otherwise = Nothing +{-# INLINABLE apply2' #-} + +pure (mkApplyInstance <$> [1..150]) + + +instance Apply Foldable fs => Foldable (Sum fs) where + foldMap f = apply @Foldable (foldMap f) + {-# INLINABLE foldMap #-} + + foldr combine seed = apply @Foldable (foldr combine seed) + {-# INLINABLE foldr #-} + + foldl combine seed = apply @Foldable (foldl combine seed) + {-# INLINABLE foldl #-} + + null = apply @Foldable null + {-# INLINABLE null #-} + + length = apply @Foldable length + {-# INLINABLE length #-} + +instance Apply Functor fs => Functor (Sum fs) where + fmap f = apply' @Functor (\ reinject a -> reinject (fmap f a)) + {-# INLINABLE fmap #-} + + (<$) v = apply' @Functor (\ reinject a -> reinject (v <$ a)) + {-# INLINABLE (<$) #-} + +instance (Apply Foldable fs, Apply Functor fs, Apply Traversable fs) => Traversable (Sum fs) where + traverse f = apply' @Traversable (\ reinject a -> reinject <$> traverse f a) + {-# INLINABLE traverse #-} + + sequenceA = apply' @Traversable (\ reinject a -> reinject <$> sequenceA a) + {-# INLINABLE sequenceA #-} + + +instance Apply Eq1 fs => Eq1 (Sum fs) where + liftEq eq u1 u2 = fromMaybe False (apply2 @Eq1 (liftEq eq) u1 u2) + {-# INLINABLE liftEq #-} + +instance (Apply Eq1 fs, Eq a) => Eq (Sum fs a) where + (==) = eq1 + {-# INLINABLE (==) #-} + + +instance (Apply Eq1 fs, Apply Ord1 fs) => Ord1 (Sum fs) where + liftCompare compareA u1@(Sum n1 _) u2@(Sum n2 _) = fromMaybe (compare n1 n2) (apply2 @Ord1 (liftCompare compareA) u1 u2) + {-# INLINABLE liftCompare #-} + +instance (Apply Eq1 fs, Apply Ord1 fs, Ord a) => Ord (Sum fs a) where + compare = compare1 + {-# INLINABLE compare #-} + + +instance Apply Show1 fs => Show1 (Sum fs) where + liftShowsPrec sp sl d = apply @Show1 (liftShowsPrec sp sl d) + {-# INLINABLE liftShowsPrec #-} + +instance (Apply Show1 fs, Show a) => Show (Sum fs a) where + showsPrec = showsPrec1 + {-# INLINABLE showsPrec #-} + + +instance Apply Hashable1 fs => Hashable1 (Sum fs) where + liftHashWithSalt hashWithSalt' salt u@(Sum n _) = salt `hashWithSalt` apply @Hashable1 (liftHashWithSalt hashWithSalt' n) u + {-# INLINABLE liftHashWithSalt #-} + +instance (Apply Hashable1 fs, Hashable a) => Hashable (Sum fs a) where + hashWithSalt = hashWithSalt1 + {-# INLINABLE hashWithSalt #-} diff --git a/src/Data/Sum/Templates.hs b/src/Data/Sum/Templates.hs new file mode 100644 --- /dev/null +++ b/src/Data/Sum/Templates.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} +{-# OPTIONS_HADDOCK hide #-} +module Data.Sum.Templates +( mkElemIndexTypeFamily +, mkApplyInstance +) where + +import Language.Haskell.TH +import Unsafe.Coerce (unsafeCoerce) + +mkElemIndexTypeFamily :: Integer -> Dec +mkElemIndexTypeFamily paramN = + ClosedTypeFamilyD (TypeFamilyHead elemIndex [KindedTV t functorK, KindedTV ts (AppT ListT functorK)] (KindSig (ConT nat)) Nothing) ((mkEquation <$> [0..pred paramN]) ++ errorCase) + where [elemIndex, t, ts, nat] = mkName <$> ["ElemIndex", "t", "ts", "Nat"] + functorK = AppT (AppT ArrowT StarT) StarT + mkT = VarT . mkName . ('t' :) . show + mkEquation i = TySynEqn [ mkT i, typeListT WildCardT (mkT <$> [0..i]) ] (LitT (NumTyLit i)) + typeErrN = mkName "TypeError" + textN = mkName "Text" + next = mkName ":<>:" + above = mkName ":$$:" + shw = mkName "ShowType" + errorCase = [ TySynEqn + [ VarT t , VarT ts ] + (AppT + (ConT typeErrN) + (AppT + (AppT (PromotedT above) + (AppT (AppT (PromotedT next) + (AppT (AppT + (PromotedT next) + (AppT (PromotedT textN) (LitT (StrTyLit "'")))) + (AppT (PromotedT shw) (VarT t)))) + (AppT (PromotedT textN) (LitT (StrTyLit "' is not a member of the type-level list"))))) + (AppT (PromotedT shw) (VarT ts)))) + ] + + +mkApplyInstance :: Integer -> Dec +mkApplyInstance paramN = + InstanceD Nothing (AppT constraint <$> typeParams) (AppT (AppT (ConT applyC) constraint) (typeListT PromotedNilT typeParams)) + [ FunD apply (zipWith mkClause [0..] typeParams) + , PragmaD (InlineP apply Inlinable FunLike AllPhases) + ] + where typeParams = VarT . mkName . ('f' :) . show <$> [0..pred paramN] + [applyC, apply, f, r, union] = mkName <$> ["Apply", "apply", "f", "r", "Sum"] + [constraint, a] = VarT . mkName <$> ["constraint", "a"] + mkClause i nthType = Clause + [ VarP f, ConP union [ LitP (IntegerL i), VarP r ] ] + (NormalB (AppE (VarE f) (SigE (AppE (VarE 'unsafeCoerce) (VarE r)) (AppT nthType a)))) + [] + +typeListT :: Type -> [Type] -> Type +typeListT = foldr (AppT . AppT PromotedConsT)