packages feed

open-witness 0.5 → 0.6

raw patch · 22 files changed

+553/−519 lines, 22 filesdep ~basedep ~constraintsdep ~hashable

Dependency ranges changed: base, constraints, hashable, random, template-haskell, transformers, witness

Files

LICENSE view
@@ -1,4 +1,4 @@-open-witness is Copyright (c) Ashley Yakeley, 2007-2017.+open-witness is Copyright (c) Ashley Yakeley, 2007-2021. All rights reserved.  Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+ changelog.md view
@@ -0,0 +1,6 @@+## [0.6] - 2022-05-10+- update for witness-0.6+- move module hierarchy+- Witnessed now synonym for PairType IOWitness++## [0.5] - 2020-09-22
open-witness.cabal view
@@ -1,65 +1,113 @@-cabal-version: 1.12+cabal-version: 2.2 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack------ hash: 7516f7597d94f8af9fcb38c8766714ce8f0b42b800a0bb156405959cc29af6a8  name:           open-witness-version:        0.5+version:        0.6 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 2008 draft paper /Witnesses and Open Witnesses/ (<https://semantic.org/wp-content/uploads/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+copyright:      (c) 2017-2022 Ashley Yakeley+license:        BSD-2-Clause license-file:   LICENSE build-type:     Simple+extra-source-files:+    changelog.md  library+  exposed-modules:+      Data.Type.OpenWitness+      Data.Type.OpenWitness.TypeRep+      Data.Type.OpenWitness.Typeable+      Data.Type.OpenWitness.Dynamic+      Data.Type.OpenWitness.Exception+      Data.Type.OpenWitness.ST+      Data.Type.OpenWitness.Instance+      Data.Type.OpenWitness.Witnessed   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+  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+      base >=4.15 && <5+    , constraints >=0.13+    , hashable >=1.3+    , random >=1.2+    , template-haskell >=2.17+    , transformers >=0.5+    , witness >=0.6   default-language: Haskell2010  test-suite tests   type: exitcode-stdio-1.0   main-is: Main.hs+  other-modules:+      Object   hs-source-dirs:       test-  default-extensions: RankNTypes EmptyDataDecls GeneralizedNewtypeDeriving ScopedTypeVariables GADTs FlexibleContexts MultiParamTypeClasses TemplateHaskell+  default-extensions:+      RankNTypes+      EmptyDataDecls+      GeneralizedNewtypeDeriving+      ScopedTypeVariables+      GADTs+      FlexibleContexts+      MultiParamTypeClasses+      TemplateHaskell   build-depends:-      base >=4.12+      base >=4.15 && <5     , mtl     , open-witness     , tasty     , tasty-hunit     , witness-  other-modules:-      Object   default-language: Haskell2010
− src/Data/OpenWitness.hs 
@@ -1,150 +0,0 @@-{-# OPTIONS -fno-warn-name-shadowing #-}--module Data.OpenWitness-    ( 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 :: forall ka kb (a :: ka) (b :: kb). a :~~: b-unsafeSameType = unsafeCoerce HRefl--unsafeWEQ :: forall k (a :: k) (b :: k). WOrder a b-unsafeWEQ = unsafeCoerce WEQ---- | 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---- type role OpenWitness nominal nominal -- doesn't compile-type role OpenWitness nominal _--instance Eq (OpenWitness s a) where-    (MkOpenWitness p) == (MkOpenWitness q) = p == q--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--instance TestOrder (OpenWitness s) where-    testOrder (MkOpenWitness ua) (MkOpenWitness ub) =-        case compare ua ub of-            LT -> WLT-            EQ -> unsafeWEQ-            GT -> WGT---- | 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 _ = []--hashOpenWitness :: Hashable t => OpenWitness s a -> t -> OpenWitness s a-hashOpenWitness (MkOpenWitness i) t = MkOpenWitness $ fromIntegral $ hash (i, t)
− src/Data/OpenWitness/Dynamic.hs 
@@ -1,50 +0,0 @@--- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.-module Data.OpenWitness.Dynamic where--import Data.Kind-import Data.OpenWitness.TypeRep-import Data.OpenWitness.Typeable-import Data.Type.Heterogeneous-import Data.Witness-import Prelude---- * The @Dynamic@ type-type Dynamic = AnyValue TypeRep---- * Converting to and from @Dynamic@-toDyn ::-       forall (a :: Type). Typeable a-    => a-    -> Dynamic-toDyn = MkAnyValue typeRep--fromDyn :: Typeable a => Dynamic -> a -> a-fromDyn dyn def =-    case fromDynamic dyn of-        Just a -> a-        _ -> def--fromDynamic ::-       forall (a :: Type). Typeable a-    => Dynamic-    -> Maybe a-fromDynamic (MkAnyValue uq a) = do-    Refl <- testEquality uq (typeRep :: TypeRep a)-    return a---- * 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"--dynTypeRep :: Dynamic -> AnyW (TypeRep :: Type -> Type)-dynTypeRep (MkAnyValue r _) = MkAnyW r
− src/Data/OpenWitness/Exception.hs 
@@ -1,49 +0,0 @@-{-# LANGUAGE DeriveDataTypeable #-}-{-# OPTIONS -fno-warn-unused-matches #-}--module Data.OpenWitness.Exception-    ( Exn-    , declexn-    , throw-    , catch-    ) where--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---- | A key to match exceptions. The type variable is the data the exception carries.-newtype Exn (e :: Type) =-    MkExn (IOWitness e)--instance TestEquality Exn where-    testEquality (MkExn a) (MkExn b) = testEquality a b--newtype ExnException =-    MkExnException (AnyValue 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 (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 
@@ -1,17 +0,0 @@-module Data.OpenWitness.Instance where--import Data.Constraint-import Data.OpenWitness.TypeRep-import Data.Type.Equality-import Data.Type.Heterogeneous-import Prelude--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 
@@ -1,12 +0,0 @@-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 
@@ -1,61 +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 Control.Monad.Fix-import Control.Monad.Trans.Class-import Control.Monad.Trans.State-import Data.OpenWitness-import Data.Witness.WitnessDict-import Prelude--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 s = OpenWitness s--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-        _ -> error "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 
@@ -1,22 +0,0 @@-module Data.OpenWitness.TypeRep where--import Data.Kind-import Data.OpenWitness-import Data.Type.Heterogeneous-import Data.Witness-import Prelude--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 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 TestEquality TypeRep where-    testEquality wa wb = fmap homoHetEq $ testHetEquality wa wb
− src/Data/OpenWitness/Typeable.hs 
@@ -1,87 +0,0 @@--- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.-module Data.OpenWitness.Typeable where--import Data.Kind-import Data.OpenWitness-import Data.OpenWitness.TypeRep-import Data.Witness-import Prelude---- | types of kind @Type@ 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 :: Type) (b :: Type). (Typeable a, Typeable b)-    => a-    -> Maybe b-cast a = do-    Refl :: a :~: b <- testEquality typeRep typeRep-    return a--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@ 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 :: Type) (k2 :: Type) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a)-mkAppTy = ApplyTypeRep
− src/Data/OpenWitness/Witnessed.hs 
@@ -1,34 +0,0 @@-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/OpenWitness.hs view
@@ -0,0 +1,149 @@+{-# OPTIONS -fno-warn-name-shadowing #-}++module Data.Type.OpenWitness+    ( 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.Int+import Data.Kind+import Data.List ((\\), union)+import Data.Traversable+import Data.Type.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 :: forall ka kb (a :: ka) (b :: kb). a :~~: b+unsafeSameType = unsafeCoerce HRefl++unsafeWEQ :: forall k (a :: k) (b :: k). WOrdering a b+unsafeWEQ = unsafeCoerce WEQ++-- | 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). Int64 -> OpenWitness s a++-- type role OpenWitness nominal nominal -- doesn't compile+type role OpenWitness nominal _++instance Eq (OpenWitness s a) where+    (MkOpenWitness p) == (MkOpenWitness q) = p == q++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 hetHomoEq $ testHetEquality wa wb++instance TestOrder (OpenWitness s) where+    testCompare (MkOpenWitness ua) (MkOpenWitness ub) =+        case compare ua ub of+            LT -> WLT+            EQ -> unsafeWEQ+            GT -> WGT++-- | The @s@ type for running 'OW' in 'IO'.+data RealWorld++-- | An 'OpenWitness' for 'IO'.+type IOWitness = OpenWitness RealWorld++ioWitnessSource :: MVar Int64+{-# 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 (succ val)+    return (MkOpenWitness val)++type OWState = Int64++-- | 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, succ val)))++-- | 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.+unsafeIOWitnessFromInt64 :: Int64 -> IOWitness a+unsafeIOWitnessFromInt64 = 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 = unsafeIOWitnessFromInt64 . 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 :: Int64 <- 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 Specificity -> 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/Type/OpenWitness/Dynamic.hs view
@@ -0,0 +1,49 @@+-- | This is an approximate re-implementation of "Data.Dynamic" using open witnesses.+module Data.Type.OpenWitness.Dynamic where++import Data.Kind+import Data.Type.OpenWitness.TypeRep+import Data.Type.OpenWitness.Typeable+import Data.Type.Witness+import Prelude++-- * The @Dynamic@ type+type Dynamic = SomeOf TypeRep++-- * Converting to and from @Dynamic@+toDyn ::+       forall (a :: Type). Typeable a+    => a+    -> Dynamic+toDyn = MkSomeOf typeRep++fromDyn :: Typeable a => Dynamic -> a -> a+fromDyn dyn def =+    case fromDynamic dyn of+        Just a -> a+        _ -> def++fromDynamic ::+       forall (a :: Type). Typeable a+    => Dynamic+    -> Maybe a+fromDynamic (MkSomeOf uq a) = do+    Refl <- testEquality uq (typeRep :: TypeRep a)+    return a++-- * Applying functions of dynamic type+dynApply :: Dynamic -> Dynamic -> Maybe Dynamic+dynApply (MkSomeOf (ApplyTypeRep (ApplyTypeRep repFn' rx') ry) f) (MkSomeOf rx x) = do+    HRefl <- testHetEquality repFn' (typeRep :: TypeRep (->))+    HRefl <- testHetEquality rx' rx+    return (MkSomeOf 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 -> Some (TypeRep :: Type -> Type)+dynTypeRep (MkSomeOf r _) = MkSome r
+ src/Data/Type/OpenWitness/Exception.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# OPTIONS -fno-warn-unused-matches #-}++module Data.Type.OpenWitness.Exception+    ( Exn+    , declexn+    , throw+    , catch+    ) where++import qualified Control.Exception as CE (Exception, catch, throw)+import Data.Kind+import Data.Type.OpenWitness+import Data.Type.Witness+import Data.Typeable+import Language.Haskell.TH hiding (Type)+import Prelude++-- | A key to match exceptions. The type variable is the data the exception carries.+newtype Exn (e :: Type) =+    MkExn (IOWitness e)++instance TestEquality Exn where+    testEquality (MkExn a) (MkExn b) = testEquality a b++newtype ExnException =+    MkExnException (SomeOf 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 (MkSomeOf exn e))++catch :: IO a -> Exn e -> (e -> IO a) -> IO a+catch foo exn catcher =+    CE.catch+        foo+        (\ex@(MkExnException cell) ->+             case matchSomeOf exn cell of+                 Just e -> catcher e+                 _ -> CE.throw ex)
+ src/Data/Type/OpenWitness/Instance.hs view
@@ -0,0 +1,17 @@+module Data.Type.OpenWitness.Instance where++import Data.Constraint+import Data.Type.Equality+import Data.Type.OpenWitness.TypeRep+import Data.Type.Witness+import Prelude++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/Type/OpenWitness/ST.hs view
@@ -0,0 +1,61 @@+-- | This is an approximate re-implementation of "Control.Monad.ST" and "Data.STRef" using open witnesses.+module Data.Type.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 Control.Monad.Fix+import Control.Monad.Trans.Class+import Control.Monad.Trans.State+import Data.Type.OpenWitness+import Data.Type.Witness.Specific.WitnessMap.Of+import Prelude++type ST s = StateT (WitnessMapOf (OpenWitness s)) (OW s)++stToOW :: ST s a -> OW s a+stToOW st = evalStateT st emptyWitnessMapOf++runST :: (forall s. ST s a) -> a+runST st = runOW (stToOW st)++fixST :: (a -> ST s a) -> ST s a+fixST = mfix++type STRef s = OpenWitness s++newSTRef :: a -> ST s (STRef s a)+newSTRef a = do+    wit <- lift newOpenWitnessOW+    dict <- get+    put (witnessMapOfAdd wit a dict)+    return wit++readSTRef :: STRef s a -> ST s a+readSTRef key = do+    dict <- get+    case witnessMapOfLookup key dict of+        Just a -> return a+        _ -> error "ref not found"++writeSTRef :: forall s a. STRef s a -> a -> ST s ()+writeSTRef key newa = modify (witnessMapOfReplace key newa)++modifySTRef :: forall s a. STRef s a -> (a -> a) -> ST s ()+modifySTRef key amap = modify (witnessMapOfModify key amap)++stToIO :: ST RealWorld a -> IO a+stToIO = owToIO . stToOW
+ src/Data/Type/OpenWitness/TypeRep.hs view
@@ -0,0 +1,21 @@+module Data.Type.OpenWitness.TypeRep where++import Data.Kind+import Data.Type.OpenWitness+import Data.Type.Witness+import Prelude++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 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 TestEquality TypeRep where+    testEquality wa wb = fmap hetHomoEq $ testHetEquality wa wb
+ src/Data/Type/OpenWitness/Typeable.hs view
@@ -0,0 +1,87 @@+-- | This is an approximate re-implementation of "Data.Typeable" using open witnesses.+module Data.Type.OpenWitness.Typeable where++import Data.Kind+import Data.Type.OpenWitness+import Data.Type.OpenWitness.TypeRep+import Data.Type.Witness+import Prelude++-- | types of kind @Type@ 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 :: Type) (b :: Type). (Typeable a, Typeable b)+    => a+    -> Maybe b+cast a = do+    Refl :: a :~: b <- testEquality typeRep typeRep+    return a++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@ 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 :: Type) (k2 :: Type) (f :: k1 -> k2) (a :: k1). TypeRep f -> TypeRep a -> TypeRep (f a)+mkAppTy = ApplyTypeRep
+ src/Data/Type/OpenWitness/Witnessed.hs view
@@ -0,0 +1,29 @@+module Data.Type.OpenWitness.Witnessed+    ( Witnessed+    , unWitnessed+    , newWitnessed+    , WitnessedIORef+    , newWitnessedIORef+    ) where++import Data.IORef+import Data.Type.OpenWitness+import Data.Type.Witness+import Prelude++type Witnessed = PairType IOWitness++unWitnessed :: Witnessed f a -> f a+unWitnessed (MkPairType _ fa) = fa++newWitnessed :: f a -> IO (Witnessed f a)+newWitnessed fa = do+    wit <- newIOWitness+    return $ MkPairType wit fa++type WitnessedIORef = Witnessed IORef++newWitnessedIORef :: a -> IO (WitnessedIORef a)+newWitnessedIORef a = do+    ref <- newIORef a+    newWitnessed ref
test/Main.hs view
@@ -2,8 +2,8 @@  module Main where -import Data.OpenWitness.Exception-import Data.OpenWitness.ST+import Data.Type.OpenWitness.Exception+import Data.Type.OpenWitness.ST import Prelude import Test.Tasty import Test.Tasty.HUnit
test/Object.hs view
@@ -1,7 +1,7 @@ module Object where -import Data.OpenWitness-import Data.Witness+import Data.Type.OpenWitness+import Data.Type.Witness  data Object s =     forall a. MkObject (OpenWitness s a)