{-- 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 }; }