{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

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

-- |

-- Module      :  Data.Function.Singletons

-- Copyright   :  (C) 2016 Richard Eisenberg

-- License     :  BSD-style (see LICENSE)

-- Maintainer  :  Ryan Scott

-- Stability   :  experimental

-- Portability :  non-portable

--

-- Defines singleton versions of the definitions in @Data.Function@.

--

-- Because many of these definitions are produced by Template Haskell,

-- it is not possible to create proper Haddock documentation. Please look

-- up the corresponding operation in @Data.Function@. Also, please excuse

-- the apparent repeated variable names. This is due to an interaction

-- between Template Haskell and Haddock.

--

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


module Data.Function.Singletons (
    -- * "Prelude" re-exports

    Id, sId, Const, sConst, type (.), (%.), Flip, sFlip, type ($), (%$)
    -- * Other combinators

  , type (&), (%&), On, sOn

    -- * Defunctionalization symbols

  , IdSym0, IdSym1
  , ConstSym0, ConstSym1, ConstSym2
  , type (.@#@$), type (.@#@$$), type (.@#@$$$), type (.@#@$$$$)
  , FlipSym0, FlipSym1, FlipSym2, FlipSym3
  , type ($@#@$), type ($@#@$$), type ($@#@$$$)
  , type (&@#@$), type (&@#@$$), type (&@#@$$$)
  , OnSym0, OnSym1, OnSym2, OnSym3, OnSym4
  ) where

import Data.Singletons.TH
import GHC.Base.Singletons

$(singletonsOnly [d|
  {- GHC falls into a loop here. Not really a surprise.

  -- | @'fix' f@ is the least fixed point of the function @f@,
  -- i.e. the least defined @x@ such that @f x = x@.
  fix :: (a -> a) -> a
  fix f = let x = f x in x
  -}

  -- -| @(*) \`on\` f = \\x y -> f x * f y@.

  --

  -- Typical usage: @'Data.List.sortBy' ('compare' \`on\` 'fst')@.

  --

  -- Algebraic properties:

  --

  -- -* @(*) \`on\` 'id' = (*)@ (if @(*) ∉ {⊥, 'const' ⊥}@)

  --

  -- -* @((*) \`on\` f) \`on\` g = (*) \`on\` (f . g)@

  --

  -- -* @'flip' on f . 'flip' on g = 'flip' on (g . f)@


  -- Proofs (so that I don't have to edit the test-suite):


  --   (*) `on` id

  -- =

  --   \x y -> id x * id y

  -- =

  --   \x y -> x * y

  -- = { If (*) /= _|_ or const _|_. }

  --   (*)


  --   (*) `on` f `on` g

  -- =

  --   ((*) `on` f) `on` g

  -- =

  --   \x y -> ((*) `on` f) (g x) (g y)

  -- =

  --   \x y -> (\x y -> f x * f y) (g x) (g y)

  -- =

  --   \x y -> f (g x) * f (g y)

  -- =

  --   \x y -> (f . g) x * (f . g) y

  -- =

  --   (*) `on` (f . g)

  -- =

  --   (*) `on` f . g


  --   flip on f . flip on g

  -- =

  --   (\h (*) -> (*) `on` h) f . (\h (*) -> (*) `on` h) g

  -- =

  --   (\(*) -> (*) `on` f) . (\(*) -> (*) `on` g)

  -- =

  --   \(*) -> (*) `on` g `on` f

  -- = { See above. }

  --   \(*) -> (*) `on` g . f

  -- =

  --   (\h (*) -> (*) `on` h) (g . f)

  -- =

  --   flip on (g . f)


  on :: (b -> b -> c) -> (a -> b) -> a -> a -> c
  (.*.) `on` f = \x y -> f x .*. f y
  infixl 0 `on`

  -- -| '&' is a reverse application operator.  This provides notational

  -- convenience.  Its precedence is one higher than that of the forward

  -- application operator '$', which allows '&' to be nested in '$'.

  --

  -- @since 4.8.0.0

  (&) :: a -> (a -> b) -> b
  x & f = f x
  infixl 1 &
  |])