-----------------------------------------------------------------------------
-- |
-- Module      :  Finite.Type
-- Maintainer  :  Felix Klein
--
-- Type association to pass types via functions.
--
-----------------------------------------------------------------------------

{-# LANGUAGE

    ImplicitParams
  , ConstraintKinds

  #-}

-----------------------------------------------------------------------------

module Finite.Type
  ( T
  , FiniteBounds
  , (#)
  , (\#)
  , (<<#)
  , (#<<)
  , t2v
  , v2t
  ) where

-----------------------------------------------------------------------------

-- | A better looking constraint specifier.

type FiniteBounds b = (?bounds :: b)

-----------------------------------------------------------------------------

-- | A type dummy.

newtype T a = T ()

-----------------------------------------------------------------------------

-- | The type dummy instance.

(#) :: T a
# :: T a
(#) = () -> T a
forall a. () -> T a
T ()

-----------------------------------------------------------------------------

-- | A type dummy returning function. Intended to use the type engine
-- for accessing the type of the argument. Note that "@(\\#) :: a -> T
-- a@" is just a special instance.

(\#) :: b -> T a
\# :: b -> T a
(\#) b
_ = T a
forall a. T a
(#)

-----------------------------------------------------------------------------

-- | Get some undefined value of the given type. Intended to be used
-- for extracting type information of polymorph types only.

t2v :: T a -> a
t2v :: T a -> a
t2v T a
_ = a
forall a. HasCallStack => a
undefined

-----------------------------------------------------------------------------

-- | Replace a function's argument by its type dummy. Intended to be used
-- for extracting type information of polymorph types only.

infixr <<#

(<<#) :: (a -> b) -> T a -> b
<<# :: (a -> b) -> T a -> b
(<<#) a -> b
f T a
_ = a -> b
f a
forall a. HasCallStack => a
undefined

-----------------------------------------------------------------------------

-- | Get the type of a given value.

v2t :: a -> T a
v2t :: a -> T a
v2t = a -> T a
forall b a. b -> T a
(\#)

-----------------------------------------------------------------------------

-- | Replace a function's dummy type argument with its value taking
-- equivalent.

infixr #<<

(#<<) :: (T a -> b) -> a -> b
#<< :: (T a -> b) -> a -> b
(#<<) T a -> b
f a
_ = T a -> b
f (T a -> b) -> T a -> b
forall a b. (a -> b) -> a -> b
$ () -> T a
forall a. () -> T a
T ()

-----------------------------------------------------------------------------