{--
JVM-Bridge -- bridge from FP languages and others to the Java VM
Copyright (C) 2001 Ashley Yakeley <ashley@semantic.org>

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
--}

module Data.Witness where
{
	newtype ID a = ID {unID :: a};

	class Witness w where
	{
		withWitness :: forall r. (forall a. (Is w a) => w a -> r) -> (forall b. w b -> r);
	};

	class (Witness w) => Is w a where
	{
		witness :: w a;
	};

	getWitness :: (Is w a) => a -> w a;
	getWitness _ = witness;

	rewitness :: (Is w a) => p a -> w a;
	rewitness _ = witness;

	class (Witness w) => TotalWitness w where
	{
		matchWitnessF :: forall f a b. w a -> w b -> Maybe (f a -> f b);
	};

	matchIsF :: (TotalWitness w,Is w a,Is w b) => Type (w ()) -> Maybe (f a -> f b);
	matchIsF t = matchWitnessF (foo t) (foo t) where
	{
		foo :: (Is w a) => Type (w ()) -> w a;
		foo _ = witness;
	};

	matchWitness :: (TotalWitness w) => w a -> w b -> Maybe (a -> b);
	matchWitness wa wb = matchWitnessF wa wb >>= (\mapF -> return (unID . mapF . ID));

	matchIs :: (TotalWitness w,Is w a,Is w b) => Type (w ()) -> Maybe (a -> b);
	matchIs t = matchIsF t >>= (\mapF -> return (unID . mapF . ID));

	data Type a = Type;

	instance Eq (Type a) where
	{
		Type == Type = True;
	};
	
	instance Witness Type where
	{
		withWitness f t = f t;
	};
	
	instance Is Type a where
	{
		witness = Type;
	};
	
	data Any w where
	{
		Any :: forall a. (Is w a) => a -> Any w
	};
	
	data AnyF w f where
	{
		AnyF :: forall a. (Is w a) => f a -> AnyF w f
	};
	
	data AnyWitness w where
	{
		AnyWitness :: forall a. w a -> AnyWitness w
	};
}