{- Data/Metrology/Set.hs

   The units Package
   Copyright (c) 2013 Richard Eisenberg
   rae@cs.brynmawr.edu

   Defines set-like operations on type-level lists.
-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Metrology.Set
-- Copyright   :  (C) 2013 Richard Eisenberg
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- This module defines a few set-like operations on type-level lists. It
-- may be applicable beyond the units package.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators,
             UndecidableInstances #-}

module Data.Metrology.Set where

import GHC.Exts ( Constraint )

-- | Are two lists equal, when considered as sets?
type family SetEqual (as :: [k]) (bs :: [k]) :: Constraint where
  SetEqual as bs = (Subset as bs, Subset bs as)

-- | Is one list a subset of the other?
type family Subset (as :: [k]) (bs :: [k]) :: Constraint where
  Subset '[] bs = (() :: Constraint)
  Subset (a ': as) bs = (a `Elem` bs, as `Subset` bs)

-- | Is an element contained in a list?
type family Elem (a :: k) (bs :: [k]) :: Constraint where
  Elem a (a ': bs) = (() :: Constraint)
  Elem a (b ': bs) = a `Elem` bs