{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} -- {-# LANGUAGE TypeFamilies #-} -- | Constructing singleton collections. module Agda.Utils.Singleton where import Data.Hashable (Hashable) import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Map (Map) import qualified Data.Map as Map import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Set (Set) import qualified Data.Set as Set class Singleton el coll | coll -> el where singleton :: el -> coll instance Singleton a (Maybe a) where singleton = Just instance Singleton a [a] where singleton = (:[]) instance Singleton a (Seq a) where singleton = Seq.singleton instance Singleton a (Set a) where singleton = Set.singleton instance Singleton Int IntSet where singleton = IntSet.singleton instance Singleton (k ,a) (Map k a) where singleton = uncurry Map.singleton instance Singleton (Int,a) (IntMap a) where singleton = uncurry IntMap.singleton instance Hashable a => Singleton a (HashSet a) where singleton = HashSet.singleton instance Hashable k => Singleton (k,a) (HashMap k a) where singleton = uncurry HashMap.singleton -- Testing newtype-deriving: -- newtype Wrap c = Wrap c -- deriving (Singleton k) -- Succeeds -- Type family version: -- class Singleton c where -- type Elem c -- singleton :: Elem c -> c -- instance Singleton [a] where -- type Elem [a] = a -- singleton = (:[]) -- instance Singleton (Maybe a) where -- type Elem (Maybe a) = a -- singleton = Just -- instance Singleton (Set a) where -- type Elem (Set a) = a -- singleton = Set.singleton -- instance Singleton (Map k a) where -- type Elem (Map k a) = (k,a) -- singleton = uncurry Map.singleton -- newtype Wrap a = Wrap a -- deriving (Singleton) -- Fails