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