{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- No overlapping instances!

-- An application of the comparison of types by their shape:
-- distinguishing function types from any other types
-- when implementing vector spaces as function spaces.
-- See isFunction.lhs for the origin of the problem
-- and the ad hoc solution.

-- This code demonstrates the mixing of functional relations
-- with type functions (i.e., associated type families).
-- The functional relations TypeEq and Normalize are defined with
-- overlapping instances -- the extension that is incompatible with
-- type functions. Although overlapping instances are encapsulated
-- in the module ConEQ, we are forced to use functional relations,
-- which are hard to mix with type functions.

-- We are still able to mix functional relations with type functions,
-- with difficulty and verbosity. When we later define the type shape
-- comparison without resorting to OverlappingInstances, we could use type
-- functions throughout, and implement functional vector spaces
-- much more concisely and clearly.

module NotAFunction where

import ConEQ (TypeEq, Normalize, HTrue, HFalse)

-- Define operations on vector spaces

--   vector addition
(<+>) :: (Annotate v annv, Vspace (Ann annv v)) => v -> v -> v
x <+> y = unAnn (annotate x `add` annotate y)

--   scalar-vector multiplication
(*>)  :: (Annotate v annv, Vspace (Ann annv v)) => 
	 ScalarF (Ann annv v) -> v -> v
x *> y = unAnn (x `mul` annotate y)

-- A type class with an associated type family, which tells the scalar field
-- of the vector space
class Vspace v where
    type ScalarF v :: *
    add  :: v -> v -> v
    mul  :: ScalarF v -> v -> v

-- A wrapper around the type x adding the phantom annotation ann
-- The wrapper has no run-time representation
newtype Ann ann x = Ann{unAnn:: x}
-- An annotation for scalars (which are any type but an arrow type)
newtype Scalar x = Scalar x

-- To avoid overlapping, Vspace is defined on annotated types.
-- The annotation disambiguates scalars from vectors (i.e., functions)

-- degenerate case: scalar field
instance Num a => Vspace (Ann (Scalar a) a) where
    type ScalarF (Ann (Scalar a) a) = a
    add (Ann x) (Ann y) = Ann (x + y)
    mul s (Ann y)       = Ann (s * y)

instance Vspace (Ann annv v) => Vspace (Ann (a->annv) (a->v)) where
    type ScalarF (Ann (a->annv) (a->v)) = ScalarF (Ann annv v)
    add (Ann f) (Ann g) = 
	Ann (\x -> unAnn ((Ann (f x) :: Ann annv v) `add` Ann (g x)))
    mul s (Ann g) = 
	Ann (\x -> unAnn (s `mul` (Ann (g x) :: Ann annv v)))


annotate :: Annotate t annt => t -> Ann annt t
annotate = Ann

-- Type-level--only computation of the annotation
class Annotate t annt | t -> annt

instance (Normalize t tn, TypeEq tn (()->()) f, Annotate' f t annt)
    => Annotate t annt

class Annotate' f t annt | f t -> annt

instance Annotate' HFalse t (Scalar t)

instance Annotate t annt => Annotate' HTrue (a->t) (a->annt)


-- Tests, taken verbatim from isFunction.lhs

test1 = (1::Int) <+> 2
-- 3

test2 = ((\x -> x <+> (10::Int)) <+> (\x -> x <+> (10::Int))) 1
-- 22

test3 = ((\x y -> x <+> y) <+> (\x y -> (x <+> y) <+> x)) (1::Int) (2::Int)
-- 7
 
test4 = ((\x y -> x <+> y) <+> (\x y -> ((2 *> x) <+> (3 *> y))))
 	(1::Int) (2::Int)
-- 11