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