I have been playing around with Nikita Volkov’s Refined library. Refined provides composable type level combinators for building smart constructors refining an existing type.

It can be considerably more convenient for simple cases to just express new types as a refinement than going through the effort of defining new datatypes and writing half a dozen extra instances and a validator.

Set membership with Singletons

The Singletons package combined with the kitchen sink of language extensions considerably increases the practical power of the type system.

Refined is missing many combinators limiting its functionality. One such example is the ability to check if a value exists in a type level list.

import Refined
import Data.Typeable (Typeable, typeOf)
import Control.Monad (unless)
import Data.Singletons.Prelude hiding (Elem)
import Data.List (elem)
import Numeric.Natural (Natural)

-- Type level list wrapper
data Elem (x :: [a]) deriving (Typeable)

-- Refined Predicate
instance forall a b (x :: [a]).
  ( Demote a ~ b -- Equality constraint
  , SingI x      -- Implicit sing parameter
  , SingKind a   -- For sing type to base type
  , Typeable a   -- Required by Refined
  , Typeable x   -- Required by Refined
  , Eq b         -- For membership comparison
  ) => Predicate (Elem x) b where
  validate p v = unless (elem v $ fromSing (sing :: Sing x)) $
    throwRefineOtherException (typeOf p) "Elem is not in list"

Singletons combined with Refined allow these set membership smart constructors to be created.

Refined with our new Elem predicate

Now that we have Elem we can use it with the rest of Refined. Here we have a type allowing 1, 3, 5, and anything over 25.

type MyNum = Refined (Or (Elem '[1, 3, 5]) (GreaterThan 25)) Natural

main = print (refine 3 :: Either RefineException MyNum)

Similarly we can use the power of refined to exclude a set of elements.

type MySecondNum = Refined (Not (Elem '[2, 3, 5, 7, 11])) Natural