{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- No overlapping instances!

-- Pattern-matching on types: distinguishing function types from
-- any other types, to implement vector spaces as function spaces

-- See isFunction.lhs for the origin of the problem
-- and its ad hoc solution. See NotAFunction.hs for the
-- solution using TypeEq and Normalize implemented
-- with overlapping instances.

-- This code is a version of NotAFunction.hs that has no
-- traces, even indirect, of overlapping instances. This present
-- code will work even if OverlappingInstances never existed.
-- We use the TTypeable's type matching to distinguish
-- an arrow type from any other type. 

-- Unlike NotAFunction.hs, we are no longer forced to use
-- type classes with functional dependencies.
-- With type functions throughout, the implementation
-- is most straightforward.

module NotAFunctionT where

import TTypeable (TYPEOF, TREPEQW, ANY, HTrue, HFalse)

-- Define operations on vector spaces
-- with vector addition and scalar-vector multiplication

-- A type class with an associated type family that tells the scalar field
-- of the vector space
class Vspace v where
    type ScalarF v :: *
    (<+>) :: v -> v -> v
    (*>)  :: ScalarF v -> v -> v

-- The test for not-a-function is most straightforward
type IsArrow t = TREPEQW (TYPEOF t) (TYPEOF (ANY->ANY))

-- All the work is done by the auxiliary Vspace', with an
-- extra parameter, a type-level Boolean that tells if the type 
-- v is an arrow type.
-- This extra parameter removes overlapping

instance (f ~ (IsArrow v), Vspace' f v) => Vspace v where
    type ScalarF v = ScalarF' (IsArrow v) v
    (<+>) = add (undefined::f)
    (*>)  = mul (undefined::f)

class Vspace' f v where
    type ScalarF' f v :: *
    add  :: f -> v -> v -> v
    mul  :: f -> ScalarF' f v -> v -> v

-- Degenerate case: scalar field
instance Num a => Vspace' HFalse a where
    type ScalarF' HFalse a = a
    add _ = (+)
    mul _ = (*)

-- Inductive case: vector field
instance Vspace v => Vspace' HTrue (a->v) where
    type ScalarF' HTrue (a->v) = ScalarF v
    add _ f g = \x -> f x <+> g x
    mul _ s g = \x -> s *> g x


-- 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