packages feed

open-witness 0.3.1 → 0.4

raw patch · 18 files changed

+625/−477 lines, 18 filesdep +constraintsdep +mtldep +open-witnessdep ~basedep ~witness

Dependencies added: constraints, mtl, open-witness, tasty, tasty-hunit

Dependency ranges changed: base, witness

Files

− Data/OpenWitness.hs 
@@ -1,134 +0,0 @@-{-# OPTIONS -fno-warn-name-shadowing #-}-module Data.OpenWitness-(-    OpenWitness,-    RealWorld,IOWitness,newIOWitness,-    OW,newOpenWitnessOW,runOW,owToIO,---    unsafeIOWitnessFromInteger,---    unsafeIOWitnessFromString,-    iowitness-) where-{-    import Prelude;-    import Data.List;-    import System.Random;-    import Language.Haskell.TH;-    import Unsafe.Coerce;-    import System.IO.Unsafe (unsafePerformIO);-    import Control.Concurrent.MVar;-    import Control.Monad.Fix;-    import Control.Monad.Trans.State;-    import Data.Functor.Identity;-    import Data.Traversable;-    import Data.Hashable;-    import Data.Witness;---    unsafeSameType :: a :~: b;-    unsafeSameType = unsafeCoerce Refl;--    -- | A witness type that can witness to any type.-    -- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.-    ;-    newtype OpenWitness s (a :: k) = MkOpenWitness Integer deriving Eq;--    instance TestEquality (OpenWitness s) where-    {-        testEquality (MkOpenWitness ua) (MkOpenWitness ub) =-            if ua == ub then Just unsafeSameType else Nothing;-    };--    -- | The @s@ type for running 'OW' in 'IO'.-    ;-    data RealWorld;--    -- | An 'OpenWitness' for 'IO'.-    ;-    type IOWitness = OpenWitness RealWorld;--    ioWitnessSource :: MVar Integer;-    {-# NOINLINE ioWitnessSource #-};-    ioWitnessSource = unsafePerformIO (newMVar 0);--    -- | Generate a new 'IOWitness' in 'IO'.-    ;-    newIOWitness :: forall a. IO (IOWitness a);-    newIOWitness = do-    {-        val <- takeMVar ioWitnessSource;-        putMVar ioWitnessSource (val + 1);-        return (MkOpenWitness val);-    };--    type OWState = Integer;--    -- | A runnable monad in which 'OpenWitness' values can be generated.-    -- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.-    ;-    newtype OW s a = MkOW (State OWState a) deriving (Functor,Applicative,Monad,MonadFix);--    -- | Run an 'OW' computation.-    ;-    runOW :: forall a. (forall s. OW s a) -> a;-    runOW uw = (\(MkOW st) -> evalState st 0) uw;--    -- | Generate a new 'OpenWitness' in 'OW'.-    ;-    newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);-    newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));--    -- | Run an 'OW' computation in 'IO'.-    ;-    owToIO :: OW RealWorld a -> IO a;-    owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let-    {-        (a,count) = runState st start;-    } in return (count,a));--    -- | An unsafe hack to generate 'IOWitness' values.-    -- This is safe if you use a different integer each time, and if @a@ is a single type.-    ;-    unsafeIOWitnessFromInteger :: Integer -> IOWitness a;-    unsafeIOWitnessFromInteger = MkOpenWitness;--    -- | An unsafe hack to generate 'IOWitness' values.-    -- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.-    ;-    unsafeIOWitnessFromString :: String -> IOWitness a;-    unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hash;--    -- | Template Haskell function to declare 'IOWitness' values.-    ;-    iowitness :: TypeQ -> Q Exp;-    iowitness qt = do-    {-        t <- qt;-        _ <- forM (freevarsType t) (\v -> reportError ("Type variable "++(show v)++" free in iowitness type"));-        l <- location;-        rnd :: Integer <- runIO randomIO;-        key <- return ((showLoc l) ++ "/" ++ (show rnd));-        keyExpr <- return (LitE (StringL key));-        untypedWitExpr <- [| unsafeIOWitnessFromString $(return keyExpr) |];-        [| $(return untypedWitExpr) :: IOWitness $(return t) |];-    } where-    {-        showLoc :: Loc -> String;-        showLoc l = (loc_filename l) ++ "=" ++ (loc_package l) ++ ":" ++ (loc_module l) ++ (show (loc_start l)) ++ (show (loc_end l));--        unionList :: (Eq a) => [[a]] -> [a];-        unionList [] = [];-        unionList (l:ls) = union l (unionList ls);--        bindingvarTVB :: TyVarBndr -> Name;-        bindingvarTVB (PlainTV n) = n;-        bindingvarTVB (KindedTV n _) = n;--        freevarsType :: Language.Haskell.TH.Type -> [Name];-        freevarsType (ForallT tvbs ps t) =-         (union (freevarsType t) (unionList (fmap freevarsType ps))) \\ (fmap bindingvarTVB tvbs);-        freevarsType (VarT name) = [name];-        freevarsType (AppT t1 t2) = union (freevarsType t1) (freevarsType t2);-        freevarsType (SigT t _) = freevarsType t;-        freevarsType _ = [];-    };-}
− Data/OpenWitness/Dynamic.hs 
@@ -1,56 +0,0 @@--- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.-module Data.OpenWitness.Dynamic where-{-{--    import Data.Witness;-    import Data.OpenWitness.OpenRep;-    import Data.OpenWitness.Typeable;--    -- * The @Dynamic@ type-    ;--    type Dynamic = Any OpenRep;--    -- * Converting to and from @Dynamic@-    ;--    toDyn :: Typeable a => a -> Dynamic;-    toDyn = MkAny rep;--    fromDyn :: Typeable a => Dynamic -> a -> a;-    fromDyn dyn def = case fromDynamic dyn of-    {-        Just a -> a;-        _ -> def;-    };--    fromDynamic :: forall a. Typeable a => Dynamic -> Maybe a;-    fromDynamic (MkAny uq a) = do-    {-        MkEqualType <- testEquality uq (rep :: OpenRep a);-        return a;-    };--    -- * Applying functions of dynamic type-    ;--    dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;-    dynApply (MkAny (ApplyOpenRep (ApplyOpenRep1 repFn' rx') ry) f) (MkAny rx x) = do-    {-        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));-        MkEqualType <- testEquality rx' rx;-        return (MkAny ry (f x));-    };-    dynApply _ _ = Nothing;--    dynApp :: Dynamic -> Dynamic -> Dynamic;-    dynApp a b = case (dynApply a b) of-    {-        Just d -> d;-        _ -> error "Type error in dynamic application.\nCan't apply function to argument";-    };--    dynTypeRep :: Dynamic -> TypeRep;-    dynTypeRep (MkAny r _) = MkAnyWitness r;--}-}
− Data/OpenWitness/Exception.hs 
@@ -1,48 +0,0 @@-{-# LANGUAGE DeriveDataTypeable #-}-{-# OPTIONS -fno-warn-unused-matches #-}-module Data.OpenWitness.Exception-(-    Exn, declexn, throw, catch-) where-{-    import Data.OpenWitness;-    import Data.Witness;-    import Data.Maybe;-    import Data.Typeable;-    import Language.Haskell.TH;-    import qualified Control.Exception as CE (Exception,throw,catch);-    import Prelude(IO,Show(..));--    -- | A key to match exceptions. The type variable is the data the exception carries.-    ;-    newtype Exn (e :: *) = MkExn (IOWitness e);--    instance TestEquality Exn where-    {-        testEquality (MkExn a) (MkExn b) = testEquality a b;-    };--    newtype ExnException = MkExnException (Any Exn) deriving Typeable;--    -- | Template Haskell function to declare 'Exn' exception keys.-    ;-    declexn :: TypeQ -> Q Exp;-    declexn te = [| MkExn $(iowitness te) |];--    instance Show ExnException where-    {-        show _ = "ExnException";-    };--    instance CE.Exception ExnException;--    throw :: Exn e -> e -> a;-    throw exn e = CE.throw (MkExnException (MkAny exn e));--    catch :: IO a -> Exn e -> (e -> IO a) -> IO a;-    catch foo exn catcher = CE.catch foo (\ex@(MkExnException cell) -> case matchAny exn cell of-    {-        Just e -> catcher e;-        _ -> CE.throw ex;-    });-}
− Data/OpenWitness/OpenRep.hs 
@@ -1,70 +0,0 @@-module Data.OpenWitness.OpenRep where-{---    import Data.Witness;---    import Data.OpenWitness;---    import Data.Maybe;-{--        data T2 (a :: * -> * -> *);--    data OpenRep2 p where-    {-        SimpleOpenRep2 :: IOWitness (T2 p) -> OpenRep2 p;---        ApplyOpenRep2 :: OpenRep3 p -> OpenRep a -> OpenRep2 (p a);-    };--    matchOpenRep2 :: OpenRep2 a -> OpenRep2 b -> Maybe (EqualType (T2 a) (T2 b));-    matchOpenRep2 (SimpleOpenRep2 wa) (SimpleOpenRep2 wb) = testEquality wa wb;-{--    matchOpenRep2 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do-    {-        MkEqualType <- matchOpenRep2 tfa tfb;-        MkEqualType <- testEquality ta tb;-        return MkEqualType;-    };-    matchOpenRep2 _ _ = Nothing;--}--        data T1 (a :: * -> *);--    data OpenRep1 p where-    {-        SimpleOpenRep1 :: IOWitness (T1 p) -> OpenRep1 p;-        ApplyOpenRep1 :: OpenRep2 p -> OpenRep a -> OpenRep1 (p a);-    };--    matchOpenRep1 :: OpenRep1 a -> OpenRep1 b -> Maybe (EqualType (T1 a) (T1 b));-    matchOpenRep1 (SimpleOpenRep1 wa) (SimpleOpenRep1 wb) = testEquality wa wb;-    matchOpenRep1 (ApplyOpenRep1 tfa ta) (ApplyOpenRep1 tfb tb) = do-    {-        MkEqualType <- matchOpenRep2 tfa tfb;-        MkEqualType <- testEquality ta tb;-        return MkEqualType;-    };-    matchOpenRep1 _ _ = Nothing;--}--{--    data OpenRep :: k -> * where-    {-        SimpleOpenRep :: IOWitness a -> OpenRep a;-        ApplyOpenRep :: OpenRep p -> OpenRep a -> OpenRep (p a);-    };--    instance TestEquality OpenRep where-    {-        testEquality (SimpleOpenRep wa) (SimpleOpenRep wb) = testEquality wa wb;-        testEquality (ApplyOpenRep tfa ta) (ApplyOpenRep tfb tb) = do-        {-            MkEqualType <- testEquality tfa tfb;-            MkEqualType <- testEquality ta tb;-            return MkEqualType;-        };-        testEquality _ _ = Nothing;-    };--    instance Eq1 OpenRep where-    {-        equals1 r1 r2 = isJust (testEquality r1 r2);-    };--}-}
− Data/OpenWitness/ST.hs 
@@ -1,59 +0,0 @@--- | This is an approximate re-implementation of "Control.Monad.ST" and "Data.STRef" using open witnesses.-module Data.OpenWitness.ST-(-    -- * The @ST@ Monad-    ST,runST,fixST,-    -- * Converting @ST@ to @OW@ and @IO@-    stToOW,RealWorld,stToIO,-    -- * STRefs-    STRef,newSTRef,readSTRef,writeSTRef,modifySTRef-) where-{-    import Data.OpenWitness;-    import Data.Witness.WitnessDict;-    import Control.Monad.Trans.State;-    import Control.Monad.Trans.Class;-    import Control.Monad.Fix;--    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);--    stToOW :: ST s a -> OW s a;-    stToOW st = evalStateT st emptyWitnessDict;--    runST :: (forall s . ST s a) -> a;-    runST st = runOW (stToOW st);--    fixST :: (a -> ST s a) -> ST s a;-    fixST = mfix;--    type STRef = OpenWitness;--    newSTRef :: a -> ST s (STRef s a);-    newSTRef a = do-    {-        wit <- lift newOpenWitnessOW;-        dict <- get;-        put (witnessDictAdd wit a dict);-        return wit;-    };--    readSTRef :: STRef s a -> ST s a;-    readSTRef key = do-    {-        dict <- get;-        case witnessDictLookup key dict of-        {-            Just a -> return a;-            _ -> fail "ref not found";-        };-    };--    writeSTRef :: forall s a. STRef s a -> a -> ST s ();-    writeSTRef key newa = modify (witnessDictReplace key newa);--    modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();-    modifySTRef key amap = modify (witnessDictModify key amap);--    stToIO :: ST RealWorld a -> IO a;-    stToIO = owToIO . stToOW;-}
− Data/OpenWitness/Typeable.hs 
@@ -1,102 +0,0 @@--- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.-module Data.OpenWitness.Typeable where-{-{--    import Data.OpenWitness.OpenRep;-    import Data.OpenWitness;-    import Data.Witness;--    -- | types of kind @*@ with a representation-    ;-    class Typeable a where-    {-        rep :: OpenRep a;-    };--    -- | types of kind @* -> *@ with a representation-    ;-    class Typeable1 t where-    {-        rep1 :: OpenRep1 t;-    };--    -- | types of kind @* -> * -> *@ with a representation-    ;-    class Typeable2 t where-    {-        rep2 :: OpenRep2 t;-    };--    instance (Typeable1 f,Typeable a) => Typeable (f a) where-    {-        rep = ApplyOpenRep rep1 rep;-    };--    instance (Typeable2 f,Typeable a) => Typeable1 (f a) where-    {-        rep1 = ApplyOpenRep1 rep2 rep;-    };--    instance Typeable2 (->) where-    {-        rep2 = SimpleOpenRep2 $(iowitness [t|T2 (->)|]);-    };--    cast :: forall a b. (Typeable a,Typeable b) => a -> Maybe b;-    cast a = do-    {-        MkEqualType :: EqualType a b <- testEquality rep rep;-        return a;-    };--    gcast :: forall a b c. (Typeable a,Typeable b) => c a -> Maybe (c b);-    gcast ca = do-    {-        MkEqualType :: EqualType a b <- testEquality rep rep;-        return ca;-    };--    -- | represents a type of kind @*@-    ;-    type TypeRep = AnyWitness OpenRep;--    typeOf :: forall t. (Typeable t) => t -> TypeRep;-    typeOf _ = MkAnyWitness (rep :: OpenRep t);--    -- | represents a type of kind @* -> *@-    ;-    type TypeRep1 = AnyWitness1 OpenRep1;--    typeOf1 :: forall t a. (Typeable1 t) => t a -> TypeRep1;-    typeOf1 _ = MkAnyWitness1 (rep1 :: OpenRep1 t);--    -- | represents a type of kind @* -> * -> *@-    ;-    type TypeRep2 = AnyWitness2 OpenRep2;--    typeOf2 :: forall t a b. (Typeable2 t) => t a b -> TypeRep2;-    typeOf2 _ = MkAnyWitness2 (rep2 :: OpenRep2 t);--    -- | given representations of @a@ and @b@, make a representation of @a -> b@-    ;-    mkFunTy :: TypeRep -> TypeRep -> TypeRep;-    mkFunTy (MkAnyWitness ta) (MkAnyWitness tb) = MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 (rep2 :: OpenRep2 (->)) ta) tb);--    -- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)-    ;-    funResultTy :: TypeRep -> TypeRep -> Maybe TypeRep;-    funResultTy (MkAnyWitness (ApplyOpenRep (ApplyOpenRep1 repFn' ta') tb')) (MkAnyWitness ta) = do-    {-        MkEqualType <- matchOpenRep2 repFn' (rep2 :: OpenRep2 (->));-        MkEqualType <- testEquality ta' ta;-        return (MkAnyWitness tb');-    };-    funResultTy _ _ = Nothing;--    mkAppTy :: TypeRep1 -> TypeRep -> TypeRep;-    mkAppTy (MkAnyWitness1 tf) (MkAnyWitness ta) = MkAnyWitness (ApplyOpenRep tf ta);--    mkAppTy1 :: TypeRep2 -> TypeRep -> TypeRep1;-    mkAppTy1 (MkAnyWitness2 tf) (MkAnyWitness ta) = MkAnyWitness1 (ApplyOpenRep1 tf ta);--}-}
LICENSE view
@@ -1,4 +1,4 @@-open-witness is Copyright (c) Ashley Yakeley, 2007-2008.+open-witness is Copyright (c) Ashley Yakeley, 2007-2017. All rights reserved.  Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
open-witness.cabal view
@@ -1,6 +1,6 @@ cabal-version:  >=1.14 name:           open-witness-version:        0.3.1+version:        0.4 x-follows-version-policy: license:        BSD3 license-file:   LICENSE@@ -17,7 +17,7 @@ build-type:     Simple  library-    hs-source-dirs: .+    hs-source-dirs: src     default-language: Haskell2010     default-extensions:         MultiParamTypeClasses@@ -30,20 +30,49 @@         TemplateHaskell         GeneralizedNewtypeDeriving         GADTs-        PolyKinds         ScopedTypeVariables+        TypeInType+        ConstraintKinds+        UndecidableInstances     build-depends:-        base >= 4.8 && < 5,+        base >= 4.9.1 && < 5,         random,         template-haskell,         transformers,         hashable,-        witness >= 0.3+        constraints,+        witness == 0.4     exposed-modules:+        Data.Type.Heterogeneous         Data.OpenWitness+        Data.OpenWitness.TypeRep+        Data.OpenWitness.Typeable         Data.OpenWitness.Dynamic         Data.OpenWitness.Exception-        Data.OpenWitness.OpenRep         Data.OpenWitness.ST-        Data.OpenWitness.Typeable+        Data.OpenWitness.Instance     ghc-options: -Wall++test-suite tests+    type: exitcode-stdio-1.0+    hs-source-dirs: test+    default-language: Haskell2010+    default-extensions:+        RankNTypes+        EmptyDataDecls+        GeneralizedNewtypeDeriving+        ScopedTypeVariables+        GADTs+        FlexibleContexts+        MultiParamTypeClasses+        TemplateHaskell+    build-depends:+        base,+        mtl,+        witness,+        open-witness,+        tasty,+        tasty-hunit+    main-is: Main.hs+    other-modules:+        Object
+ src/Data/OpenWitness.hs view
@@ -0,0 +1,144 @@+{-# OPTIONS -fno-warn-name-shadowing #-}+module Data.OpenWitness+(+    OpenWitness,+    RealWorld,IOWitness,newIOWitness,+    OW,newOpenWitnessOW,runOW,owToIO,+--    unsafeIOWitnessFromInteger,+--    unsafeIOWitnessFromString,+    iowitness+) where+{+    import Prelude;+    import Data.Kind;+    import Data.List;+    import System.Random;+    import Language.Haskell.TH;+    import Unsafe.Coerce;+    import System.IO.Unsafe (unsafePerformIO);+    import Control.Concurrent.MVar;+    import Control.Monad.Fix;+    import Control.Monad.Trans.State;+    import Data.Functor.Identity;+    import Data.Traversable;+    import Data.Hashable;+    import Data.Witness;+    import Data.Type.Heterogeneous;+++    unsafeSameType :: HetEq a b;+    unsafeSameType = unsafeCoerce ReflH;++    -- | A witness type that can witness to any type.+    -- But values cannot be constructed; they can only be generated in 'IO' and certain other monads.+    ;+    newtype OpenWitness :: * -> forall (k :: *). k -> * where+    {+        MkOpenWitness :: Integer -> OpenWitness s a;+    } deriving Eq;++    instance TestHetEquality (OpenWitness s) where+    {+        testHetEquality (MkOpenWitness ua) (MkOpenWitness ub) =+            if ua == ub then Just unsafeSameType else Nothing;+    };++    instance TestEquality (OpenWitness s) where+    {+        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;+    };++    -- | The @s@ type for running 'OW' in 'IO'.+    ;+    data RealWorld;++    -- | An 'OpenWitness' for 'IO'.+    ;+    type IOWitness = OpenWitness RealWorld;++    ioWitnessSource :: MVar Integer;+    {-# NOINLINE ioWitnessSource #-};+    ioWitnessSource = unsafePerformIO (newMVar 0);++    -- | Generate a new 'IOWitness' in 'IO'.+    ;+    newIOWitness :: forall a. IO (IOWitness a);+    newIOWitness = do+    {+        val <- takeMVar ioWitnessSource;+        putMVar ioWitnessSource (val + 1);+        return (MkOpenWitness val);+    };++    type OWState = Integer;++    -- | A runnable monad in which 'OpenWitness' values can be generated.+    -- The @s@ parameter plays the same role as it does in 'ST', preventing 'OpenWitness' values from one run being used in another.+    ;+    newtype OW s a = MkOW (State OWState a) deriving (Functor,Applicative,Monad,MonadFix);++    -- | Run an 'OW' computation.+    ;+    runOW :: forall a. (forall s. OW s a) -> a;+    runOW uw = (\(MkOW st) -> evalState st 0) uw;++    -- | Generate a new 'OpenWitness' in 'OW'.+    ;+    newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);+    newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));++    -- | Run an 'OW' computation in 'IO'.+    ;+    owToIO :: OW RealWorld a -> IO a;+    owToIO (MkOW st) = modifyMVar ioWitnessSource (\start -> let+    {+        (a,count) = runState st start;+    } in return (count,a));++    -- | An unsafe hack to generate 'IOWitness' values.+    -- This is safe if you use a different integer each time, and if @a@ is a single type.+    ;+    unsafeIOWitnessFromInteger :: Integer -> IOWitness a;+    unsafeIOWitnessFromInteger = MkOpenWitness;++    -- | An unsafe hack to generate 'IOWitness' values.+    -- This is safe if you use a different string each time (and 'hashString' doesn't collide), and if @a@ is a single type.+    ;+    unsafeIOWitnessFromString :: String -> IOWitness a;+    unsafeIOWitnessFromString = unsafeIOWitnessFromInteger . fromIntegral . hash;++    -- | Template Haskell function to declare 'IOWitness' values.+    ;+    iowitness :: TypeQ -> Q Exp;+    iowitness qt = do+    {+        t <- qt;+        _ <- forM (freevarsType t) (\v -> reportError ("Type variable "++(show v)++" free in iowitness type"));+        l <- location;+        rnd :: Integer <- runIO randomIO;+        key <- return ((showLoc l) ++ "/" ++ (show rnd));+        keyExpr <- return (LitE (StringL key));+        untypedWitExpr <- [| unsafeIOWitnessFromString $(return keyExpr) |];+        [| $(return untypedWitExpr) :: IOWitness $(return t) |];+    } where+    {+        showLoc :: Loc -> String;+        showLoc l = (loc_filename l) ++ "=" ++ (loc_package l) ++ ":" ++ (loc_module l) ++ (show (loc_start l)) ++ (show (loc_end l));++        unionList :: (Eq a) => [[a]] -> [a];+        unionList [] = [];+        unionList (l:ls) = union l (unionList ls);++        bindingvarTVB :: TyVarBndr -> Name;+        bindingvarTVB (PlainTV n) = n;+        bindingvarTVB (KindedTV n _) = n;++        freevarsType :: Language.Haskell.TH.Type -> [Name];+        freevarsType (ForallT tvbs ps t) =+         (union (freevarsType t) (unionList (fmap freevarsType ps))) \\ (fmap bindingvarTVB tvbs);+        freevarsType (VarT name) = [name];+        freevarsType (AppT t1 t2) = union (freevarsType t1) (freevarsType t2);+        freevarsType (SigT t _) = freevarsType t;+        freevarsType _ = [];+    };+}
+ src/Data/OpenWitness/Dynamic.hs view
@@ -0,0 +1,56 @@+-- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.+module Data.OpenWitness.Dynamic where+{+    import Data.Kind;+    import Data.Witness;+    import Data.Type.Heterogeneous;+    import Data.OpenWitness.TypeRep;+    import Data.OpenWitness.Typeable;++    -- * The @Dynamic@ type+    ;++    type Dynamic = Any TypeRep;++    -- * Converting to and from @Dynamic@+    ;++    toDyn :: forall (a :: *). Typeable a => a -> Dynamic;+    toDyn = MkAny typeRep;++    fromDyn :: Typeable a => Dynamic -> a -> a;+    fromDyn dyn def = case fromDynamic dyn of+    {+        Just a -> a;+        _ -> def;+    };++    fromDynamic :: forall (a :: *). Typeable a => Dynamic -> Maybe a;+    fromDynamic (MkAny uq a) = do+    {+        Refl <- testEquality uq (typeRep :: TypeRep a);+        return a;+    };++    -- * Applying functions of dynamic type+    ;++    dynApply :: Dynamic -> Dynamic -> Maybe Dynamic;+    dynApply (MkAny (ApplyTypeRep (ApplyTypeRep repFn' rx') ry) f) (MkAny rx x) = do+    {+        ReflH <- testHetEquality repFn' (typeRep :: TypeRep (->));+        ReflH <- testHetEquality rx' rx;+        return (MkAny ry (f x));+    };+    dynApply _ _ = Nothing;++    dynApp :: Dynamic -> Dynamic -> Dynamic;+    dynApp a b = case (dynApply a b) of+    {+        Just d -> d;+        _ -> error "Type error in dynamic application.\nCan't apply function to argument";+    };++    dynTypeRep :: Dynamic -> AnyWitness (TypeRep :: * -> *);+    dynTypeRep (MkAny r _) = MkAnyWitness r;+}
+ src/Data/OpenWitness/Exception.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# OPTIONS -fno-warn-unused-matches #-}+module Data.OpenWitness.Exception+(+    Exn, declexn, throw, catch+) where+{+    import Data.Kind;+    import Data.OpenWitness;+    import Data.Witness;+    import Data.Maybe;+    import Data.Typeable;+    import Language.Haskell.TH;+    import qualified Control.Exception as CE (Exception,throw,catch);+    import Prelude(IO,Show(..));++    -- | A key to match exceptions. The type variable is the data the exception carries.+    ;+    newtype Exn (e :: *) = MkExn (IOWitness e);++    instance TestEquality Exn where+    {+        testEquality (MkExn a) (MkExn b) = testEquality a b;+    };++    newtype ExnException = MkExnException (Any Exn) deriving Typeable;++    -- | Template Haskell function to declare 'Exn' exception keys.+    ;+    declexn :: TypeQ -> Q Exp;+    declexn te = [| MkExn $(iowitness te) |];++    instance Show ExnException where+    {+        show _ = "ExnException";+    };++    instance CE.Exception ExnException;++    throw :: Exn e -> e -> a;+    throw exn e = CE.throw (MkExnException (MkAny exn e));++    catch :: IO a -> Exn e -> (e -> IO a) -> IO a;+    catch foo exn catcher = CE.catch foo (\ex@(MkExnException cell) -> case matchAny exn cell of+    {+        Just e -> catcher e;+        _ -> CE.throw ex;+    });+}
+ src/Data/OpenWitness/Instance.hs view
@@ -0,0 +1,17 @@+module Data.OpenWitness.Instance where+{+    import Data.Kind;+    import Data.Constraint;+    import Data.Type.Heterogeneous;+    import Data.OpenWitness.TypeRep;++    data Instance = forall (t :: Constraint). t => MkInstance (TypeRep t);++    findInstance :: [Instance] -> TypeRep t -> Maybe (Dict t);+    findInstance [] _ = Nothing;+    findInstance (MkInstance ti:ii) t = case testHetEquality ti t of+    {+        Just ReflH -> Just Dict;+        Nothing -> findInstance ii t;+    };+}
+ src/Data/OpenWitness/ST.hs view
@@ -0,0 +1,59 @@+-- | This is an approximate re-implementation of "Control.Monad.ST" and "Data.STRef" using open witnesses.+module Data.OpenWitness.ST+(+    -- * The @ST@ Monad+    ST,runST,fixST,+    -- * Converting @ST@ to @OW@ and @IO@+    stToOW,RealWorld,stToIO,+    -- * STRefs+    STRef,newSTRef,readSTRef,writeSTRef,modifySTRef+) where+{+    import Data.OpenWitness;+    import Data.Witness.WitnessDict;+    import Control.Monad.Trans.State;+    import Control.Monad.Trans.Class;+    import Control.Monad.Fix;++    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);++    stToOW :: ST s a -> OW s a;+    stToOW st = evalStateT st emptyWitnessDict;++    runST :: (forall s . ST s a) -> a;+    runST st = runOW (stToOW st);++    fixST :: (a -> ST s a) -> ST s a;+    fixST = mfix;++    type STRef = OpenWitness;++    newSTRef :: a -> ST s (STRef s a);+    newSTRef a = do+    {+        wit <- lift newOpenWitnessOW;+        dict <- get;+        put (witnessDictAdd wit a dict);+        return wit;+    };++    readSTRef :: STRef s a -> ST s a;+    readSTRef key = do+    {+        dict <- get;+        case witnessDictLookup key dict of+        {+            Just a -> return a;+            _ -> fail "ref not found";+        };+    };++    writeSTRef :: forall s a. STRef s a -> a -> ST s ();+    writeSTRef key newa = modify (witnessDictReplace key newa);++    modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();+    modifySTRef key amap = modify (witnessDictModify key amap);++    stToIO :: ST RealWorld a -> IO a;+    stToIO = owToIO . stToOW;+}
+ src/Data/OpenWitness/TypeRep.hs view
@@ -0,0 +1,36 @@+module Data.OpenWitness.TypeRep where+{+    import Data.Kind;+    import Data.Maybe;+    import Data.Witness;+    import Data.OpenWitness;+    import Data.Type.Heterogeneous;++    data TypeRep :: forall (k :: *). k -> * where+    {+        SimpleTypeRep :: forall (k :: *) (a :: k). IOWitness a -> TypeRep a;+        ApplyTypeRep :: forall (k1 :: *) (k2 :: *) (p :: k1 -> k2) (a :: k1). TypeRep p -> TypeRep a -> TypeRep (p a);+    };++    instance TestHetEquality TypeRep where+    {+        testHetEquality (SimpleTypeRep wa) (SimpleTypeRep wb) = testHetEquality wa wb;+        testHetEquality (ApplyTypeRep tfa ta) (ApplyTypeRep tfb tb) = do+        {+            ReflH <- testHetEquality tfa tfb;+            ReflH <- testHetEquality ta tb;+            return ReflH;+        };+        testHetEquality _ _ = Nothing;+    };++    instance TestEquality TypeRep where+    {+        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;+    };++    instance Eq1 TypeRep where+    {+        equals1 r1 r2 = isJust (testHetEquality r1 r2);+    };+}
+ src/Data/OpenWitness/Typeable.hs view
@@ -0,0 +1,120 @@+-- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.+module Data.OpenWitness.Typeable where+{+    import Data.Kind;+    import Data.OpenWitness.TypeRep;+    import Data.OpenWitness;+    import Data.Witness;++    -- | types of kind @*@ with a representation+    ;+    class Typeable (a :: k) where+    {+        typeRep :: TypeRep a;+    };++    instance (Typeable (f :: k1 -> k2),Typeable (a :: k1)) => Typeable (f a) where+    {+        typeRep = ApplyTypeRep typeRep typeRep;+    };++    instance Typeable Type where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Type|]);+    };++    type Fun = (->);++    instance Typeable (->) where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Fun|]);+    };++    instance Typeable Constraint where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Constraint|]);+    };++    instance Typeable TypeRep where+    {+        typeRep = SimpleTypeRep $(iowitness [t|TypeRep|]);+    };++    instance Typeable Typeable where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Typeable|]);+    };++    instance Typeable () where+    {+        typeRep = SimpleTypeRep $(iowitness [t|()|]);+    };++    instance Typeable (,) where+    {+        typeRep = SimpleTypeRep $(iowitness [t|(,)|]);+    };++    instance Typeable Either where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Either|]);+    };++    instance Typeable Maybe where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Maybe|]);+    };++    instance Typeable [] where+    {+        typeRep = SimpleTypeRep $(iowitness [t|[]|]);+    };++    instance Typeable Bool where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Bool|]);+    };++    instance Typeable Char where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Char|]);+    };++    instance Typeable Int where+    {+        typeRep = SimpleTypeRep $(iowitness [t|Int|]);+    };++    cast :: forall (a :: *) (b :: *). (Typeable a,Typeable b) => a -> Maybe b;+    cast a = do+    {+        Refl :: a :~: b <- testEquality typeRep typeRep;+        return a;+    };++    gcast :: forall (k :: *) (a :: k) (b :: k) (c :: k -> *). (Typeable a,Typeable b) => c a -> Maybe (c b);+    gcast ca = do+    {+        Refl :: a :~: b <- testEquality typeRep typeRep;+        return ca;+    };++    -- | given representations of @a@ and @b@, make a representation of @a -> b@+    ;+    mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b);+    mkFunTy ta tb = ApplyTypeRep (ApplyTypeRep (typeRep :: TypeRep (->)) ta) tb;++    -- | given representations of @a -> b@ and @a@, make a representation of @b@ (otherwise not)+    ;+    funResultTy :: TypeRep (a -> b) -> TypeRep a -> Maybe (TypeRep b);+    funResultTy (ApplyTypeRep (ApplyTypeRep repFn' ta') tb') ta = do+    {+        Refl <- testEquality repFn' (typeRep :: TypeRep (->));+        Refl <- testEquality ta' ta;+        return tb';+    };+    funResultTy _ _ = Nothing;++    mkAppTy :: forall (k1 :: *) (k2 :: *) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a);+    mkAppTy = ApplyTypeRep;+}
+ src/Data/Type/Heterogeneous.hs view
@@ -0,0 +1,20 @@+module Data.Type.Heterogeneous where+{+    import Data.Kind;+    import Data.Type.Equality;++    data HetEq (a :: ka) (b :: kb) where+    {+        ReflH :: forall (k :: *) (t :: k). HetEq t t;+    };++    -- | somewhat awkwardly named+    ;+    homoHetEq :: forall (k :: *) (a :: k) (b :: k). HetEq a b -> a :~: b;+    homoHetEq ReflH = Refl;++    class TestHetEquality (w :: forall k. k -> *) where+    {+        testHetEquality :: forall (ka :: *) (a :: ka) (kb :: *) (b :: kb). w a -> w b -> Maybe (HetEq a b);+    };+}
+ test/Main.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE TemplateHaskell #-}+module Main where+{+    import Data.OpenWitness.ST;+    import Data.OpenWitness.Exception;+    import Prelude;+    import Test.Tasty;+    import Test.Tasty.HUnit;++    stuff :: ST s [Int];+    stuff = do+    {+        ra <- newSTRef 3;+        a1 <- readSTRef ra;+        rb <- newSTRef 4;+        b1 <- readSTRef rb;+        writeSTRef ra 5;+        a2 <- readSTRef ra;+        writeSTRef rb 7;+        b2 <- readSTRef rb;+        return [a1,b1,a2,b2];+    };++    testST :: TestTree;+    testST = testCase "ST" $ assertEqual "vals" [3,4,5,7] $ runST stuff;++    intExn :: Exn Int;+    intExn = $(declexn [t|Int|]);+    stringExn :: Exn String;+    stringExn = $(declexn [t|String|]);++    data Caught = NotCaught | IntCaught Int | StringCaught String deriving (Eq,Show);++    getCaught :: IO a -> IO Caught;+    getCaught f = ((do+    {+        _ <- f;+        return NotCaught;+    }+    `catch` intExn) (\x -> return (IntCaught x))+    `catch` stringExn) (\x -> return (StringCaught x));++    testCaught :: String -> Caught -> IO a -> TestTree;+    testCaught name expected f = testCase name $ do+    {+        result <- getCaught f;+        assertEqual "caught" expected result;+    };++    tests :: TestTree;+    tests = testGroup "test"+    [+        testST,+        testCaught "return" NotCaught $ return "hello",+        testCaught "throw intExn 3" (IntCaught 3) $ throw intExn 3,+        testCaught "throw stringExn text" (StringCaught "text") $ throw stringExn "text",+        testCaught "throw intExn 67" (IntCaught 67) $ throw intExn 67,+        testCaught "throw stringExn str" (StringCaught "str") $ throw stringExn "str"+    ];++    main :: IO ();+    main = defaultMain tests;+}
+ test/Object.hs view
@@ -0,0 +1,24 @@+module Object where+{+	import Data.Witness;+	import Data.OpenWitness;++	data Object s = forall a. MkObject (OpenWitness s a) a;++	matchObject :: OpenWitness s b -> Object s -> Maybe b;+	matchObject uqb (MkObject uqa a) = do+	{+		MkEqualType <- testEquality uqa uqb;+		return a;+	};++	makeConversions :: OpenWitness s b -> (b -> Object s,Object s -> Maybe b);+	makeConversions wit = (MkObject wit,matchObject wit);++	getConversions :: OW s (b -> Object s,Object s -> Maybe b);+	getConversions = do+	{+		wit <- newOpenWitnessOW;+		return (makeConversions wit);+	};+}