packages feed

open-witness 0.4.0.1 → 0.5

raw patch · 14 files changed

+523/−558 lines, 14 filesdep ~basedep ~witnesssetup-changed

Dependency ranges changed: base, witness

Files

Setup.hs view
@@ -1,2 +1,3 @@ import Distribution.Simple+ main = defaultMain
open-witness.cabal view
@@ -1,78 +1,65 @@-cabal-version:  >=1.14+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 7516f7597d94f8af9fcb38c8766714ce8f0b42b800a0bb156405959cc29af6a8+ name:           open-witness-version:        0.4.0.1-x-follows-version-policy:-license:        BSD3-license-file:   LICENSE-copyright:      Ashley Yakeley <ashley@semantic.org>-author:         Ashley Yakeley <ashley@semantic.org>-maintainer:     Ashley Yakeley <ashley@semantic.org>-homepage:       https://github.com/AshleyYakeley/open-witness-bug-reports:    https://github.com/AshleyYakeley/open-witness/issues+version:        0.5 synopsis:       open witnesses-description:-    Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad.-    See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>).+description:    Open witnesses are witnesses that can witness to any type. However, they cannot be constructed, they can only be generated in the IO monad. See the paper /Witnesses and Open Witnesses/ (<http://semantic.org/stuff/Open-Witnesses.pdf>). category:       Data+homepage:       https://github.com/AshleyYakeley/open-witness+bug-reports:    https://github.com/AshleyYakeley/open-witness/issues+author:         Ashley Yakeley+maintainer:     <ashley@semantic.org>+copyright:      (c) 2017-2019 Ashley Yakeley+license:        BSD3+license-file:   LICENSE build-type:     Simple  library-    hs-source-dirs: src-    default-language: Haskell2010-    default-extensions:-        MultiParamTypeClasses-        RankNTypes-        FlexibleContexts-        TypeOperators-        FlexibleInstances-        EmptyDataDecls-        KindSignatures-        TemplateHaskell-        GeneralizedNewtypeDeriving-        GADTs-        ScopedTypeVariables-        TypeInType-        ConstraintKinds-        UndecidableInstances-    build-depends:-        base >= 4.9.1 && < 5,-        random,-        template-haskell,-        transformers,-        hashable,-        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.ST-        Data.OpenWitness.Instance-    ghc-options: -Wall+  hs-source-dirs:+      src+  default-extensions: AllowAmbiguousTypes Arrows ConstraintKinds DataKinds DefaultSignatures EmptyCase EmptyDataDecls ExistentialQuantification FlexibleContexts FlexibleInstances ForeignFunctionInterface FunctionalDependencies GADTs GeneralizedNewtypeDeriving ImplicitParams NoImplicitPrelude InstanceSigs KindSignatures LambdaCase MultiParamTypeClasses OverloadedLabels OverloadedStrings PartialTypeSignatures PatternGuards PatternSynonyms PolyKinds RankNTypes RecordWildCards RecursiveDo RoleAnnotations ScopedTypeVariables StandaloneDeriving NoStarIsType TemplateHaskell TypeApplications TypeFamilies TypeFamilyDependencies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses ViewPatterns+  ghc-options: -Wall -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat -Wnoncanonical-monad-instances+  build-depends:+      base >=4.14 && <5+    , constraints+    , hashable+    , random+    , template-haskell+    , transformers+    , witness >=0.5+  exposed-modules:+      Data.OpenWitness.Order+      Data.OpenWitness+      Data.OpenWitness.TypeRep+      Data.OpenWitness.Typeable+      Data.OpenWitness.Dynamic+      Data.OpenWitness.Exception+      Data.OpenWitness.ST+      Data.OpenWitness.Instance+      Data.OpenWitness.Witnessed+  other-modules:+      Paths_open_witness+  default-language: Haskell2010  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+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs:+      test+  default-extensions: RankNTypes EmptyDataDecls GeneralizedNewtypeDeriving ScopedTypeVariables GADTs FlexibleContexts MultiParamTypeClasses TemplateHaskell+  build-depends:+      base >=4.12+    , mtl+    , open-witness+    , tasty+    , tasty-hunit+    , witness+  other-modules:+      Object+  default-language: Haskell2010
src/Data/OpenWitness.hs view
@@ -1,149 +1,150 @@ {-# 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;+    ( OpenWitness+    , RealWorld+    , IOWitness+    , newIOWitness+    , OW+    , newOpenWitnessOW+    , runOW+    , owToIO+    , iowitness+    , hashOpenWitness+    ) where +import Control.Concurrent.MVar+import Control.Monad.Fix+import Control.Monad.Trans.State+import Data.Functor.Identity+import Data.Hashable+import Data.Kind+import Data.List ((\\), union)+import Data.OpenWitness.Order+import Data.Traversable+import Data.Type.Heterogeneous+import Data.Witness+import Language.Haskell.TH hiding (Type)+import qualified Language.Haskell.TH+import Prelude+import System.IO.Unsafe (unsafePerformIO)+import System.Random+import Unsafe.Coerce -    unsafeSameType :: HetEq a b;-    unsafeSameType = unsafeCoerce ReflH;+unsafeSameType :: forall ka kb (a :: ka) (b :: kb). a :~~: b+unsafeSameType = unsafeCoerce HRefl -    -- | 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;-    };+unsafeWEQ :: forall k (a :: k) (b :: k). WOrder a b+unsafeWEQ = unsafeCoerce WEQ -    instance Eq (OpenWitness s a) where-    {-        (MkOpenWitness p) == (MkOpenWitness q) = p == q;-    };+-- | 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 :: Type -> forall (k :: Type). k -> Type where+    MkOpenWitness :: forall (k :: Type) (s :: Type) (a :: k). Integer -> OpenWitness s a -    instance TestHetEquality (OpenWitness s) where-    {-        testHetEquality (MkOpenWitness ua) (MkOpenWitness ub) =-            if ua == ub then Just unsafeSameType else Nothing;-    };+-- type role OpenWitness nominal nominal -- doesn't compile+type role OpenWitness nominal _ -    instance TestEquality (OpenWitness s) where-    {-        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;-    };+instance Eq (OpenWitness s a) where+    (MkOpenWitness p) == (MkOpenWitness q) = p == q -    -- | The @s@ type for running 'OW' in 'IO'.-    ;-    data RealWorld;+instance TestHetEquality (OpenWitness s) where+    testHetEquality (MkOpenWitness ua) (MkOpenWitness ub) =+        if ua == ub+            then Just unsafeSameType+            else Nothing -    -- | An 'OpenWitness' for 'IO'.-    ;-    type IOWitness = OpenWitness RealWorld;+instance TestEquality (OpenWitness s) where+    testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb -    ioWitnessSource :: MVar Integer;-    {-# NOINLINE ioWitnessSource #-};-    ioWitnessSource = unsafePerformIO (newMVar 0);+instance TestOrder (OpenWitness s) where+    testOrder (MkOpenWitness ua) (MkOpenWitness ub) =+        case compare ua ub of+            LT -> WLT+            EQ -> unsafeWEQ+            GT -> WGT -    -- | Generate a new 'IOWitness' in 'IO'.-    ;-    newIOWitness :: forall a. IO (IOWitness a);-    newIOWitness = do-    {-        val <- takeMVar ioWitnessSource;-        putMVar ioWitnessSource (val + 1);-        return (MkOpenWitness val);-    };+-- | The @s@ type for running 'OW' in 'IO'.+data RealWorld -    type OWState = Integer;+-- | An 'OpenWitness' for 'IO'.+type IOWitness = OpenWitness RealWorld -    -- | 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);+ioWitnessSource :: MVar Integer+{-# NOINLINE ioWitnessSource #-}+ioWitnessSource = unsafePerformIO (newMVar 0) -    -- | Run an 'OW' computation.-    ;-    runOW :: forall a. (forall s. OW s a) -> a;-    runOW uw = (\(MkOW st) -> evalState st 0) uw;+-- | Generate a new 'IOWitness' in 'IO'.+newIOWitness :: forall a. IO (IOWitness a)+newIOWitness = do+    val <- takeMVar ioWitnessSource+    putMVar ioWitnessSource (val + 1)+    return (MkOpenWitness val) -    -- | Generate a new 'OpenWitness' in 'OW'.-    ;-    newOpenWitnessOW :: forall s a. OW s (OpenWitness s a);-    newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val,val+1)));+type OWState = Integer -    -- | 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));+-- | 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) -    -- | 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;+-- | Run an 'OW' computation.+runOW :: forall a. (forall s. OW s a) -> a+runOW uw = (\(MkOW st) -> evalState st 0) uw -    -- | 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;+-- | Generate a new 'OpenWitness' in 'OW'.+newOpenWitnessOW :: forall s a. OW s (OpenWitness s a)+newOpenWitnessOW = MkOW (StateT (\val -> Identity (MkOpenWitness val, val + 1))) -    -- | 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));+-- | 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)) -        unionList :: (Eq a) => [[a]] -> [a];-        unionList [] = [];-        unionList (l:ls) = union l (unionList ls);+-- | 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 -        bindingvarTVB :: TyVarBndr -> Name;-        bindingvarTVB (PlainTV n) = n;-        bindingvarTVB (KindedTV n _) = n;+-- | 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 -        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 _ = [];-    };-}+-- | 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 _ = []++hashOpenWitness :: Hashable t => OpenWitness s a -> t -> OpenWitness s a+hashOpenWitness (MkOpenWitness i) t = MkOpenWitness $ fromIntegral $ hash (i, t)
src/Data/OpenWitness/Dynamic.hs view
@@ -1,56 +1,50 @@ -- | 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@-    ;+import Data.Kind+import Data.OpenWitness.TypeRep+import Data.OpenWitness.Typeable+import Data.Type.Heterogeneous+import Data.Witness+import Prelude -    toDyn :: forall (a :: *). Typeable a => a -> Dynamic;-    toDyn = MkAny typeRep;+-- * The @Dynamic@ type+type Dynamic = AnyValue TypeRep -    fromDyn :: Typeable a => Dynamic -> a -> a;-    fromDyn dyn def = case fromDynamic dyn of-    {-        Just a -> a;-        _ -> def;-    };+-- * Converting to and from @Dynamic@+toDyn ::+       forall (a :: Type). Typeable a+    => a+    -> Dynamic+toDyn = MkAnyValue typeRep -    fromDynamic :: forall (a :: *). Typeable a => Dynamic -> Maybe a;-    fromDynamic (MkAny uq a) = do-    {-        Refl <- testEquality uq (typeRep :: TypeRep a);-        return a;-    };+fromDyn :: Typeable a => Dynamic -> a -> a+fromDyn dyn def =+    case fromDynamic dyn of+        Just a -> a+        _ -> def -    -- * Applying functions of dynamic type-    ;+fromDynamic ::+       forall (a :: Type). Typeable a+    => Dynamic+    -> Maybe a+fromDynamic (MkAnyValue uq a) = do+    Refl <- testEquality uq (typeRep :: TypeRep a)+    return a -    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;+-- * Applying functions of dynamic type+dynApply :: Dynamic -> Dynamic -> Maybe Dynamic+dynApply (MkAnyValue (ApplyTypeRep (ApplyTypeRep repFn' rx') ry) f) (MkAnyValue rx x) = do+    HRefl <- testHetEquality repFn' (typeRep :: TypeRep (->))+    HRefl <- testHetEquality rx' rx+    return (MkAnyValue 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";-    };+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;-}+dynTypeRep :: Dynamic -> AnyW (TypeRep :: Type -> Type)+dynTypeRep (MkAnyValue r _) = MkAnyW r
src/Data/OpenWitness/Exception.hs view
@@ -1,49 +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(..));+    ( Exn+    , declexn+    , throw+    , catch+    ) where -    -- | A key to match exceptions. The type variable is the data the exception carries.-    ;-    newtype Exn (e :: *) = MkExn (IOWitness e);+import qualified Control.Exception as CE (Exception, catch, throw)+import Data.Kind+import Data.OpenWitness+import Data.Typeable+import Data.Witness+import Language.Haskell.TH hiding (Type)+import Prelude -    instance TestEquality Exn where-    {-        testEquality (MkExn a) (MkExn b) = testEquality a b;-    };+-- | A key to match exceptions. The type variable is the data the exception carries.+newtype Exn (e :: Type) =+    MkExn (IOWitness e) -    newtype ExnException = MkExnException (Any Exn) deriving Typeable;+instance TestEquality Exn where+    testEquality (MkExn a) (MkExn b) = testEquality a b -    -- | Template Haskell function to declare 'Exn' exception keys.-    ;-    declexn :: TypeQ -> Q Exp;-    declexn te = [| MkExn $(iowitness te) |];+newtype ExnException =+    MkExnException (AnyValue Exn)+    deriving (Typeable) -    instance Show ExnException where-    {-        show _ = "ExnException";-    };+-- | Template Haskell function to declare 'Exn' exception keys.+declexn :: TypeQ -> Q Exp+declexn te = [|MkExn $(iowitness te)|] -    instance CE.Exception ExnException;+instance Show ExnException where+    show _ = "ExnException" -    throw :: Exn e -> e -> a;-    throw exn e = CE.throw (MkExnException (MkAny exn e));+instance CE.Exception ExnException -    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;-    });-}+throw :: Exn e -> e -> a+throw exn e = CE.throw (MkExnException (MkAnyValue exn e))++catch :: IO a -> Exn e -> (e -> IO a) -> IO a+catch foo exn catcher =+    CE.catch+        foo+        (\ex@(MkExnException cell) ->+             case matchAnyValue exn cell of+                 Just e -> catcher e+                 _ -> CE.throw ex)
src/Data/OpenWitness/Instance.hs view
@@ -1,17 +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);+import Data.Constraint+import Data.OpenWitness.TypeRep+import Data.Type.Equality+import Data.Type.Heterogeneous+import Prelude -    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;-    };-}+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 HRefl -> Just Dict+        Nothing -> findInstance ii t
+ src/Data/OpenWitness/Order.hs view
@@ -0,0 +1,12 @@+module Data.OpenWitness.Order where++import Data.Kind+import Data.Witness++data WOrder (a :: k) (b :: k) where+    WLT :: forall k (a :: k) (b :: k). WOrder a b+    WEQ :: forall k (a :: k). WOrder a a+    WGT :: forall k (a :: k) (b :: k). WOrder a b++class TestEquality w => TestOrder (w :: k -> Type) where+    testOrder :: forall (a :: k) (b :: k). w a -> w b -> WOrder a b
src/Data/OpenWitness/ST.hs view
@@ -1,59 +1,61 @@ -- | 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,+      ST+    , runST+    , fixST     -- * Converting @ST@ to @OW@ and @IO@-    stToOW,RealWorld,stToIO,+    , 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;+    , STRef+    , newSTRef+    , readSTRef+    , writeSTRef+    , modifySTRef+    ) where -    type ST s = StateT (WitnessDict (OpenWitness s)) (OW s);+import Control.Monad.Fix+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+import Data.OpenWitness+import Data.Witness.WitnessDict+import Prelude -    stToOW :: ST s a -> OW s a;-    stToOW st = evalStateT st emptyWitnessDict;+type ST s = StateT (WitnessDict (OpenWitness s)) (OW s) -    runST :: (forall s . ST s a) -> a;-    runST st = runOW (stToOW st);+stToOW :: ST s a -> OW s a+stToOW st = evalStateT st emptyWitnessDict -    fixST :: (a -> ST s a) -> ST s a;-    fixST = mfix;+runST :: (forall s. ST s a) -> a+runST st = runOW (stToOW st) -    type STRef s = OpenWitness s;+fixST :: (a -> ST s a) -> ST s a+fixST = mfix -    newSTRef :: a -> ST s (STRef s a);-    newSTRef a = do-    {-        wit <- lift newOpenWitnessOW;-        dict <- get;-        put (witnessDictAdd wit a dict);-        return wit;-    };+type STRef s = OpenWitness s -    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";-        };-    };+newSTRef :: a -> ST s (STRef s a)+newSTRef a = do+    wit <- lift newOpenWitnessOW+    dict <- get+    put (witnessDictAdd wit a dict)+    return wit -    writeSTRef :: forall s a. STRef s a -> a -> ST s ();-    writeSTRef key newa = modify (witnessDictReplace key newa);+readSTRef :: STRef s a -> ST s a+readSTRef key = do+    dict <- get+    case witnessDictLookup key dict of+        Just a -> return a+        _ -> error "ref not found" -    modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ();-    modifySTRef key amap = modify (witnessDictModify key amap);+writeSTRef :: forall s a. STRef s a -> a -> ST s ()+writeSTRef key newa = modify (witnessDictReplace key newa) -    stToIO :: ST RealWorld a -> IO a;-    stToIO = owToIO . stToOW;-}+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
@@ -1,36 +1,22 @@ 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);-    };+import Data.Kind+import Data.OpenWitness+import Data.Type.Heterogeneous+import Data.Witness+import Prelude -    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;-    };+data TypeRep :: forall (k :: Type). k -> Type where+    SimpleTypeRep :: forall (k :: Type) (a :: k). IOWitness a -> TypeRep a+    ApplyTypeRep :: forall (k1 :: Type) (k2 :: Type) (p :: k1 -> k2) (a :: k1). TypeRep p -> TypeRep a -> TypeRep (p a) -    instance TestEquality TypeRep where-    {-        testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb;-    };+instance TestHetEquality TypeRep where+    testHetEquality (SimpleTypeRep wa) (SimpleTypeRep wb) = testHetEquality wa wb+    testHetEquality (ApplyTypeRep tfa ta) (ApplyTypeRep tfb tb) = do+        HRefl <- testHetEquality tfa tfb+        HRefl <- testHetEquality ta tb+        return HRefl+    testHetEquality _ _ = Nothing -    instance Eq1 TypeRep where-    {-        equals1 r1 r2 = isJust (testHetEquality r1 r2);-    };-}+instance TestEquality TypeRep where+    testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb
src/Data/OpenWitness/Typeable.hs view
@@ -1,120 +1,87 @@ -- | 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;-    };+import Data.Kind+import Data.OpenWitness+import Data.OpenWitness.TypeRep+import Data.Witness+import Prelude -    instance (Typeable (f :: k1 -> k2),Typeable (a :: k1)) => Typeable (f a) where-    {-        typeRep = ApplyTypeRep typeRep typeRep;-    };+-- | types of kind @Type@ with a representation+class Typeable (a :: k) where+    typeRep :: TypeRep a -    instance Typeable Type where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Type|]);-    };+instance (Typeable (f :: k1 -> k2), Typeable (a :: k1)) => Typeable (f a) where+    typeRep = ApplyTypeRep typeRep typeRep -    type Fun = (->);+instance Typeable Type where+    typeRep = SimpleTypeRep $(iowitness [t|Type|]) -    instance Typeable (->) where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Fun|]);-    };+type Fun = (->) -    instance Typeable Constraint where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Constraint|]);-    };+instance Typeable (->) where+    typeRep = SimpleTypeRep $(iowitness [t|Fun|]) -    instance Typeable TypeRep where-    {-        typeRep = SimpleTypeRep $(iowitness [t|TypeRep|]);-    };+instance Typeable Constraint where+    typeRep = SimpleTypeRep $(iowitness [t|Constraint|]) -    instance Typeable Typeable where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Typeable|]);-    };+instance Typeable TypeRep where+    typeRep = SimpleTypeRep $(iowitness [t|TypeRep|]) -    instance Typeable () where-    {-        typeRep = SimpleTypeRep $(iowitness [t|()|]);-    };+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 (,) where+    typeRep = SimpleTypeRep $(iowitness [t|(,)|]) -    instance Typeable Maybe where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Maybe|]);-    };+instance Typeable Either where+    typeRep = SimpleTypeRep $(iowitness [t|Either|]) -    instance Typeable [] where-    {-        typeRep = SimpleTypeRep $(iowitness [t|[]|]);-    };+instance Typeable Maybe where+    typeRep = SimpleTypeRep $(iowitness [t|Maybe|]) -    instance Typeable Bool where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Bool|]);-    };+instance Typeable [] where+    typeRep = SimpleTypeRep $(iowitness [t|[]|]) -    instance Typeable Char where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Char|]);-    };+instance Typeable Bool where+    typeRep = SimpleTypeRep $(iowitness [t|Bool|]) -    instance Typeable Int where-    {-        typeRep = SimpleTypeRep $(iowitness [t|Int|]);-    };+instance Typeable Char where+    typeRep = SimpleTypeRep $(iowitness [t|Char|]) -    cast :: forall (a :: *) (b :: *). (Typeable a,Typeable b) => a -> Maybe b;-    cast a = do-    {-        Refl :: a :~: b <- testEquality typeRep typeRep;-        return a;-    };+instance Typeable Int where+    typeRep = SimpleTypeRep $(iowitness [t|Int|]) -    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;-    };+cast ::+       forall (a :: Type) (b :: Type). (Typeable a, Typeable b)+    => a+    -> Maybe b+cast a = do+    Refl :: a :~: b <- testEquality typeRep typeRep+    return a -    -- | 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;+gcast ::+       forall (k :: Type) (a :: k) (b :: k) (c :: k -> Type). (Typeable a, Typeable b)+    => c a+    -> Maybe (c b)+gcast ca = do+    Refl :: a :~: b <- testEquality typeRep typeRep+    return ca -    -- | 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;+-- | 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 -    mkAppTy :: forall (k1 :: *) (k2 :: *) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a);-    mkAppTy = ApplyTypeRep;-}+-- | 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 :: Type) (k2 :: Type) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a)+mkAppTy = ApplyTypeRep
+ src/Data/OpenWitness/Witnessed.hs view
@@ -0,0 +1,34 @@+module Data.OpenWitness.Witnessed+    ( Witnessed+    , unWitnessed+    , newWitnessed+    , WitnessedIORef+    , newWitnessedIORef+    ) where++import Data.IORef+import Data.OpenWitness+import Data.Type.Equality+import Prelude++data Witnessed f a =+    MkWitnessed (IOWitness a)+                (f a)++unWitnessed :: Witnessed f a -> f a+unWitnessed (MkWitnessed _ fa) = fa++instance TestEquality (Witnessed f) where+    testEquality (MkWitnessed wa _) (MkWitnessed wb _) = testEquality wa wb++newWitnessed :: f a -> IO (Witnessed f a)+newWitnessed fa = do+    wit <- newIOWitness+    return $ MkWitnessed wit fa++type WitnessedIORef = Witnessed IORef++newWitnessedIORef :: a -> IO (WitnessedIORef a)+newWitnessedIORef a = do+    ref <- newIORef a+    newWitnessed ref
− src/Data/Type/Heterogeneous.hs 
@@ -1,20 +0,0 @@-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
@@ -1,63 +1,67 @@ {-# 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];-    };+import Data.OpenWitness.Exception+import Data.OpenWitness.ST+import Prelude+import Test.Tasty+import Test.Tasty.HUnit -    testST :: TestTree;-    testST = testCase "ST" $ assertEqual "vals" [3,4,5,7] $ runST stuff;+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] -    intExn :: Exn Int;-    intExn = $(declexn [t|Int|]);-    stringExn :: Exn String;-    stringExn = $(declexn [t|String|]);+testST :: TestTree+testST = testCase "ST" $ assertEqual "vals" [3, 4, 5, 7] $ runST stuff -    data Caught = NotCaught | IntCaught Int | StringCaught String deriving (Eq,Show);+intExn :: Exn Int+intExn = $(declexn [t|Int|]) -    getCaught :: IO a -> IO Caught;-    getCaught f = ((do-    {-        _ <- f;-        return NotCaught;-    }-    `catch` intExn) (\x -> return (IntCaught x))-    `catch` stringExn) (\x -> return (StringCaught x));+stringExn :: Exn String+stringExn = $(declexn [t|String|]) -    testCaught :: String -> Caught -> IO a -> TestTree;-    testCaught name expected f = testCase name $ do-    {-        result <- getCaught f;-        assertEqual "caught" expected result;-    };+data Caught+    = NotCaught+    | IntCaught Int+    | StringCaught String+    deriving (Eq, Show) -    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"-    ];+getCaught :: IO a -> IO Caught+getCaught f =+    ((do+          _ <- f+          return NotCaught+    `catch` intExn)+         (\x -> return (IntCaught x)) `catch`+     stringExn)+        (\x -> return (StringCaught x)) -    main :: IO ();-    main = defaultMain tests;-}+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
@@ -1,24 +1,21 @@ module Object where-{-    import Data.Witness;-    import Data.OpenWitness; -    data Object s = forall a. MkObject (OpenWitness s a) a;+import Data.OpenWitness+import Data.Witness -    matchObject :: OpenWitness s b -> Object s -> Maybe b;-    matchObject uqb (MkObject uqa a) = do-    {-        Refl <- testEquality uqa uqb;-        return a;-    };+data Object s =+    forall a. MkObject (OpenWitness s a)+                       a -    makeConversions :: OpenWitness s b -> (b -> Object s,Object s -> Maybe b);-    makeConversions wit = (MkObject wit,matchObject wit);+matchObject :: OpenWitness s b -> Object s -> Maybe b+matchObject uqb (MkObject uqa a) = do+    Refl <- testEquality uqa uqb+    return a -    getConversions :: OW s (b -> Object s,Object s -> Maybe b);-    getConversions = do-    {-        wit <- newOpenWitnessOW;-        return (makeConversions wit);-    };-}+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)