forked from github/purescript-typeable
Use polykinds in Purescript 0.14
This commit is contained in:
Anupam Jain
parent
d6a4c80b81
commit
1eabe79427
279
attic/Data.purs
Normal file
279
attic/Data.purs
Normal file
@ -0,0 +1,279 @@
|
||||
module Data.Data where
|
||||
|
||||
import Control.Alt ((<|>))
|
||||
import Control.Alternative (empty)
|
||||
import Control.Applicative (pure)
|
||||
import Control.Bind (bind, (>>=))
|
||||
import Control.Category (identity, (<<<))
|
||||
import Control.Monad (class Monad)
|
||||
import Control.MonadPlus (class MonadPlus)
|
||||
import Data.Array as A
|
||||
import Data.CommutativeRing ((+))
|
||||
import Data.Const (Const(..))
|
||||
import Data.Either (Either(..))
|
||||
import Data.Eq ((==))
|
||||
import Data.Foldable (foldl)
|
||||
import Data.Function (const, ($))
|
||||
import Data.Identity (Identity(..))
|
||||
import Data.Maybe (Maybe(..), fromMaybe, maybe)
|
||||
import Data.Newtype (unwrap)
|
||||
import Data.Ordering (Ordering)
|
||||
import Data.Tuple (Tuple(..))
|
||||
import Data.Typeable (class Tag0, class Tag1, class Typeable, cast)
|
||||
import Data.Unit (Unit)
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
mkT :: forall a b. Typeable a => Typeable b => (b -> b) -> a -> a
|
||||
mkT f = fromMaybe identity (cast f)
|
||||
|
||||
mkQ :: forall a b r. Typeable a => Typeable b => r -> (b -> r) -> a -> r
|
||||
mkQ r q a = maybe r q (cast a)
|
||||
|
||||
mkM :: forall a b m. Typeable a => Typeable b => Monad m => Tag1 m => (b -> m b) -> a -> m a
|
||||
mkM f = fromMaybe pure (cast f)
|
||||
|
||||
-- Purescript can't have cycles in typeclasses
|
||||
-- So we manually reify the dictionary into the DataDict datatype
|
||||
-- Not using wrapped records here because Purescript can't handle constraints inside records
|
||||
newtype DataDict a = DataDict
|
||||
(forall c. (forall d b. Data d => c (d -> b) -> d -> c b)
|
||||
-- ^ defines how nonempty constructor applications are
|
||||
-- folded. It takes the folded tail of the constructor
|
||||
-- application and its head, i.e., an immediate subterm,
|
||||
-- and combines them in some way.
|
||||
-> (forall g. g -> c g)
|
||||
-- ^ defines how the empty constructor application is
|
||||
-- folded, like the neutral \/ start element for list
|
||||
-- folding.
|
||||
-> a
|
||||
-- ^ structure to be folded.
|
||||
-> c a
|
||||
-- ^ result, with a type defined in terms of @a@, but
|
||||
-- variability is achieved by means of type constructor
|
||||
-- @c@ for the construction of the actual result type.
|
||||
)
|
||||
|
||||
gfoldl :: forall a c. Data a => (forall d b. Data d => c (d -> b) -> d -> c b)
|
||||
-- ^ defines how nonempty constructor applications are
|
||||
-- folded. It takes the folded tail of the constructor
|
||||
-- application and its head, i.e., an immediate subterm,
|
||||
-- and combines them in some way.
|
||||
-> (forall g. g -> c g)
|
||||
-- ^ defines how the empty constructor application is
|
||||
-- folded, like the neutral \/ start element for list
|
||||
-- folding.
|
||||
-> a
|
||||
-- ^ structure to be folded.
|
||||
-> c a
|
||||
-- ^ result, with a type defined in terms of @a@, but
|
||||
-- variability is achieved by means of type constructor
|
||||
-- @c@ for the construction of the actual result type.
|
||||
gfoldl = let DataDict f = dataDict in f
|
||||
|
||||
class Typeable a <= Data a where
|
||||
dataDict :: DataDict a
|
||||
|
||||
-- | A generic transformation that maps over the immediate subterms
|
||||
--
|
||||
-- The default definition instantiates the type constructor @c@ in the
|
||||
-- type of 'gfoldl' to an identity datatype constructor, using the
|
||||
-- isomorphism pair as injection and projection.
|
||||
gmapT :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
|
||||
|
||||
-- Use the Identity datatype constructor
|
||||
-- to instantiate the type constructor c in the type of gfoldl,
|
||||
-- and perform injections Identity and projections runIdentity accordingly.
|
||||
--
|
||||
gmapT f x0 = unwrap (gfoldl k Identity x0)
|
||||
where
|
||||
k :: forall d b. Data d => Identity (d->b) -> d -> Identity b
|
||||
k (Identity c) x = Identity (c (f x))
|
||||
|
||||
|
||||
-- | A generic query with a left-associative binary operator
|
||||
gmapQl :: forall a r r'. Data a => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
|
||||
gmapQl o r f = unwrap <<< gfoldl k z
|
||||
where
|
||||
k :: forall d b. Data d => Const r (d->b) -> d -> Const r b
|
||||
k c x = Const $ (unwrap c) `o` f x
|
||||
z :: forall g. g -> Const r g
|
||||
z _ = Const r
|
||||
|
||||
-- | A generic query with a right-associative binary operator
|
||||
gmapQr :: forall a r r'. Data a => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r
|
||||
gmapQr o r0 f x0 = unQr (gfoldl k (const (Qr identity)) x0) r0
|
||||
where
|
||||
k :: forall d b. Data d => Qr r (d->b) -> d -> Qr r b
|
||||
k (Qr c) x = Qr (\r -> c (f x `o` r))
|
||||
|
||||
|
||||
-- | A generic query that processes the immediate subterms and returns a list
|
||||
-- of results. The list is given in the same order as originally specified
|
||||
-- in the declaration of the data constructors.
|
||||
gmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> a -> Array u
|
||||
gmapQ f = gmapQr (A.cons) [] f
|
||||
|
||||
|
||||
-- | A generic query that processes one child by index (zero-based)
|
||||
gmapQi :: forall u a. Data a => Int -> (forall d. Data d => d -> u) -> a -> u
|
||||
gmapQi i f x = case gfoldl k z x of Qi _ q -> case q of
|
||||
Nothing -> unsafeCoerce "UNEXPECTED NOTHING"
|
||||
Just q' -> q'
|
||||
where
|
||||
k :: forall d b. Data d => Qi u (d -> b) -> d -> Qi u b
|
||||
k (Qi i' q) a = Qi (i'+1) (if i==i' then Just (f a) else q)
|
||||
z :: forall g q. g -> Qi q g
|
||||
z _ = Qi 0 Nothing
|
||||
|
||||
|
||||
-- | A generic monadic transformation that maps over the immediate subterms
|
||||
--
|
||||
-- The default definition instantiates the type constructor @c@ in
|
||||
-- the type of 'gfoldl' to the monad datatype constructor, defining
|
||||
-- injection and projection using 'return' and '>>='.
|
||||
gmapM :: forall m a. Data a => Monad m => (forall d. Data d => d -> m d) -> a -> m a
|
||||
|
||||
-- Use immediately the monad datatype constructor
|
||||
-- to instantiate the type constructor c in the type of gfoldl,
|
||||
-- so injection and projection is done by return and >>=.
|
||||
--
|
||||
gmapM f = gfoldl k pure
|
||||
where
|
||||
k :: forall b d. Data d => m (d -> b) -> d -> m b
|
||||
k c x = do c' <- c
|
||||
x' <- f x
|
||||
pure (c' x')
|
||||
|
||||
|
||||
-- | Transformation of at least one immediate subterm does not fail
|
||||
gmapMp :: forall m a. Data a => MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a
|
||||
|
||||
{-
|
||||
|
||||
The type constructor that we use here simply keeps track of the fact
|
||||
if we already succeeded for an immediate subterm; see Mp below. To
|
||||
this end, we couple the monadic computation with a Boolean.
|
||||
|
||||
-}
|
||||
|
||||
gmapMp f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
|
||||
if b then pure x' else empty
|
||||
where
|
||||
z :: forall g. g -> Mp m g
|
||||
z g = Mp (pure (Tuple g false))
|
||||
k :: forall d b. Data d => Mp m (d -> b) -> d -> Mp m b
|
||||
k (Mp c) y
|
||||
= Mp ( c >>= \(Tuple h b) ->
|
||||
(f y >>= \y' -> pure (Tuple (h y') true))
|
||||
<|> pure (Tuple (h y) b)
|
||||
)
|
||||
|
||||
-- | Transformation of one immediate subterm with success
|
||||
gmapMo :: forall m a. Data a => MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a
|
||||
|
||||
{-
|
||||
|
||||
We use the same pairing trick as for gmapMp,
|
||||
i.e., we use an extra Boolean component to keep track of the
|
||||
fact whether an immediate subterm was processed successfully.
|
||||
However, we cut of mapping over subterms once a first subterm
|
||||
was transformed successfully.
|
||||
|
||||
-}
|
||||
|
||||
gmapMo f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
|
||||
if b then pure x' else empty
|
||||
where
|
||||
z :: forall g. g -> Mp m g
|
||||
z g = Mp (pure (Tuple g false))
|
||||
k :: forall d b. Data d => Mp m (d -> b) -> d -> Mp m b
|
||||
k (Mp c) y
|
||||
= Mp ( c >>= \(Tuple h b) -> if b
|
||||
then pure (Tuple (h y) b)
|
||||
else (f y >>= \y' -> pure (Tuple (h y') true))
|
||||
<|> pure (Tuple (h y) b)
|
||||
)
|
||||
|
||||
|
||||
|
||||
-- | Type constructor for adding counters to queries
|
||||
data Qi q a = Qi Int (Maybe q)
|
||||
|
||||
|
||||
-- | The type constructor used in definition of gmapQr
|
||||
newtype Qr r a = Qr (r -> r)
|
||||
|
||||
unQr :: forall r a. Qr r a -> r -> r
|
||||
unQr (Qr f) = f
|
||||
|
||||
-- | The type constructor used in definition of gmapMp
|
||||
newtype Mp m x = Mp (m (Tuple x Boolean))
|
||||
|
||||
unMp :: forall m x. Mp m x -> m (Tuple x Boolean)
|
||||
unMp (Mp f) = f
|
||||
|
||||
|
||||
-- | Left-associative fold operation for constructor applications.
|
||||
--
|
||||
-- The type of 'gfoldl' is a headache, but operationally it is a simple
|
||||
-- generalisation of a list fold.
|
||||
--
|
||||
-- The default definition for 'gfoldl' is @'const' 'id'@, which is
|
||||
-- suitable for abstract datatypes with no substructures.
|
||||
-- gfoldl
|
||||
|
||||
|
||||
-- TODO: Why do we need `Tag0` here? Instead of `Typeable`.
|
||||
instance dataArray :: (Tag0 a, Data a) => Data (Array a) where
|
||||
dataDict = DataDict \k z arr -> case A.uncons arr of
|
||||
Nothing -> z []
|
||||
Just x -> (z A.cons `k` x.head) `k` x.tail
|
||||
|
||||
instance dataMaybe :: (Tag0 a, Data a) => Data (Maybe a) where
|
||||
dataDict = DataDict \k z e -> case e of
|
||||
Nothing -> z Nothing
|
||||
Just a -> z Just `k` a
|
||||
|
||||
instance dataEither :: (Tag0 a, Tag0 b, Data a, Data b) => Data (Either a b) where
|
||||
dataDict = DataDict \k z e -> case e of
|
||||
Left a -> z Left `k` a
|
||||
Right b -> z Right `k` b
|
||||
|
||||
instance dataBoolean :: Data Boolean where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataInt :: Data Int where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataNumber :: Data Number where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataChar :: Data Char where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataString :: Data String where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataUnit :: Data Unit where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
instance dataOrdering :: Data Ordering where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
|
||||
-- Combinators
|
||||
|
||||
-- | Apply a transformation everywhere, bottom-up
|
||||
everywhere :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
|
||||
everywhere f x = f (gmapT (everywhere f) x)
|
||||
|
||||
-- | Apply a transformation everywhere, top-down
|
||||
everywhere' :: forall a. Data a => (forall b. Data b => b -> b) -> a -> a
|
||||
everywhere' f x = gmapT (everywhere' f) (f x)
|
||||
|
||||
-- | Summarise all nodes in top-down, left-to-right
|
||||
everything :: forall a r. Data a => (r -> r -> r) -> (forall b. Data b => b -> r) -> a -> r
|
||||
everything k f x = foldl k (f x) (gmapQ (everything k f) x)
|
||||
|
||||
-- | Apply a monadic transformation everywhere, bottom-up
|
||||
everywhereM :: forall m a. Monad m => Data a => (forall b. Data b => b -> m b) -> a -> m a
|
||||
everywhereM f x = gmapM (everywhereM f) x >>= f
|
||||
21
attic/Dynamic.purs
Normal file
21
attic/Dynamic.purs
Normal file
@ -0,0 +1,21 @@
|
||||
module Data.Dynamic where
|
||||
|
||||
import Data.Exists (Exists, mkExists, runExists)
|
||||
import Data.Function ((#))
|
||||
import Data.Functor (map)
|
||||
import Data.Leibniz (runLeibniz)
|
||||
import Data.Maybe (Maybe)
|
||||
import Data.Typeable (class Typeable, TypeRep, eqT, typeRep)
|
||||
|
||||
-- | A `Dynamic` holds a value `a` in a context `t`
|
||||
-- | and forgets the type of `a`
|
||||
data Dynamic' t a = Dynamic' (TypeRep a) (t a)
|
||||
data Dynamic t = Dynamic (Exists (Dynamic' t))
|
||||
|
||||
-- | Wrap a value into a dynamic
|
||||
dynamic :: forall t a. Typeable a => t a -> Dynamic t
|
||||
dynamic a = Dynamic (mkExists (Dynamic' typeRep a))
|
||||
|
||||
-- | Extract a value from a dynamic
|
||||
unwrapDynamic :: forall t a. TypeRep a -> Dynamic t -> Maybe (t a)
|
||||
unwrapDynamic ta (Dynamic e) = e # runExists \(Dynamic' ti v) -> map (\w -> runLeibniz w v) (eqT ti ta)
|
||||
@ -19,7 +19,7 @@ import Data.Maybe (Maybe(..), fromMaybe, maybe)
|
||||
import Data.Newtype (unwrap)
|
||||
import Data.Ordering (Ordering)
|
||||
import Data.Tuple (Tuple(..))
|
||||
import Data.Typeable (class Tag0, class Tag1, class Typeable, cast)
|
||||
import Data.Typeable (class TagT, class Typeable, cast)
|
||||
import Data.Unit (Unit)
|
||||
import Unsafe.Coerce (unsafeCoerce)
|
||||
|
||||
@ -29,7 +29,7 @@ mkT f = fromMaybe identity (cast f)
|
||||
mkQ :: forall a b r. Typeable a => Typeable b => r -> (b -> r) -> a -> r
|
||||
mkQ r q a = maybe r q (cast a)
|
||||
|
||||
mkM :: forall a b m. Typeable a => Typeable b => Monad m => Tag1 m => (b -> m b) -> a -> m a
|
||||
mkM :: forall a b m. Typeable a => Typeable b => Monad m => TagT m => (b -> m b) -> a -> m a
|
||||
mkM f = fromMaybe pure (cast f)
|
||||
|
||||
-- Purescript can't have cycles in typeclasses
|
||||
@ -197,10 +197,12 @@ gmapMo f x = unMp (gfoldl k z x) >>= \(Tuple x' b) ->
|
||||
|
||||
|
||||
-- | Type constructor for adding counters to queries
|
||||
data Qi :: forall k. Type -> k -> Type
|
||||
data Qi q a = Qi Int (Maybe q)
|
||||
|
||||
|
||||
-- | The type constructor used in definition of gmapQr
|
||||
newtype Qr :: forall k. Type -> k -> Type
|
||||
newtype Qr r a = Qr (r -> r)
|
||||
|
||||
unQr :: forall r a. Qr r a -> r -> r
|
||||
@ -223,42 +225,42 @@ unMp (Mp f) = f
|
||||
-- gfoldl
|
||||
|
||||
|
||||
-- TODO: Why do we need `Tag0` here? Instead of `Typeable`.
|
||||
instance dataArray :: (Tag0 a, Data a) => Data (Array a) where
|
||||
-- TODO: Why do we need `TagT` here? Instead of `Typeable`.
|
||||
instance dataArray :: (TagT a, Data a) => Data (Array a) where
|
||||
dataDict = DataDict \k z arr -> case A.uncons arr of
|
||||
Nothing -> z []
|
||||
Just x -> (z A.cons `k` x.head) `k` x.tail
|
||||
|
||||
instance dataMaybe :: (Tag0 a, Data a) => Data (Maybe a) where
|
||||
instance dataMaybe :: (TagT a, Data a) => Data (Maybe a) where
|
||||
dataDict = DataDict \k z e -> case e of
|
||||
Nothing -> z Nothing
|
||||
Just a -> z Just `k` a
|
||||
|
||||
instance dataEither :: (Tag0 a, Tag0 b, Data a, Data b) => Data (Either a b) where
|
||||
instance dataEither :: (TagT a, TagT b, Data a, Data b) => Data (Either a b) where
|
||||
dataDict = DataDict \k z e -> case e of
|
||||
Left a -> z Left `k` a
|
||||
Right b -> z Right `k` b
|
||||
|
||||
instance dataBoolean :: Data Boolean where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataInt :: Data Int where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataNumber :: Data Number where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataChar :: Data Char where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataString :: Data String where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataUnit :: Data Unit where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
instance dataOrdering :: Data Ordering where
|
||||
dataDict = DataDict \k z x -> z x
|
||||
dataDict = DataDict \_ z x -> z x
|
||||
|
||||
-- Combinators
|
||||
|
||||
|
||||
@ -9,6 +9,7 @@ import Data.Typeable (class Typeable, TypeRep, eqT, typeRep)
|
||||
|
||||
-- | A `Dynamic` holds a value `a` in a context `t`
|
||||
-- | and forgets the type of `a`
|
||||
data Dynamic' :: forall k. (k -> Type) -> k -> Type
|
||||
data Dynamic' t a = Dynamic' (TypeRep a) (t a)
|
||||
data Dynamic t = Dynamic (Exists (Dynamic' t))
|
||||
|
||||
|
||||
@ -5,39 +5,18 @@ exports.typeRepDefault0 = function(t) {
|
||||
return t;
|
||||
};
|
||||
|
||||
exports.typeRepFromTag1 = pack('tag1');
|
||||
exports.typeRepFromTag1 = pack('tagT');
|
||||
|
||||
exports.showTypeRep = function(t) {
|
||||
return "" + t;
|
||||
};
|
||||
|
||||
exports.proxy0 = tag;
|
||||
exports.proxy1 = tag;
|
||||
exports.proxy2 = tag;
|
||||
exports.proxy3 = tag;
|
||||
exports.proxy4 = tag;
|
||||
exports.proxy5 = tag;
|
||||
exports.proxy6 = tag;
|
||||
exports.proxy7 = tag;
|
||||
exports.proxy8 = tag;
|
||||
exports.proxy9 = tag;
|
||||
exports.proxy10 = tag;
|
||||
exports.proxy11 = tag;
|
||||
exports.proxyT = tag;
|
||||
|
||||
// Just a JS class, instances of which can be tested for equality
|
||||
function tag() {}
|
||||
|
||||
// exports.proxy0FromTag1 = pack('tag1');
|
||||
exports.proxy1FromTag2 = pack('tag2');
|
||||
exports.proxy2FromTag3 = pack('tag3');
|
||||
exports.proxy3FromTag4 = pack('tag4');
|
||||
exports.proxy4FromTag5 = pack('tag5');
|
||||
exports.proxy5FromTag6 = pack('tag6');
|
||||
exports.proxy6FromTag7 = pack('tag7');
|
||||
exports.proxy7FromTag8 = pack('tag8');
|
||||
exports.proxy8FromTag9 = pack('tag9');
|
||||
exports.proxy9FromTag10 = pack('tag10');
|
||||
exports.proxy10FromTag11 = pack('tag11');
|
||||
exports.proxyTFromTagT = pack('tagT');
|
||||
|
||||
function pack(tagName) {
|
||||
return function(origTag) {
|
||||
@ -77,7 +56,7 @@ exports.typeRowCons = function(_) {
|
||||
exports.typeRowNil = {record: []};
|
||||
|
||||
function eqTypeRepHelper(t1,t2) {
|
||||
if(t1.tag0) return t1 === t2;
|
||||
if(t1.tagT) return t1 === t2;
|
||||
if(t1.tag !== t2.tag) return false;
|
||||
if(t1.record) {
|
||||
if(!t2.record) return false;
|
||||
|
||||
@ -15,10 +15,8 @@ module Data.Typeable
|
||||
, SomeTypeRep(..)
|
||||
, wrapSomeTypeRep
|
||||
, unwrapSomeTypeRep
|
||||
, Proxy0, Proxy1, Proxy2, Proxy3, Proxy4, Proxy5, Proxy6, Proxy7, Proxy8, Proxy9, Proxy10, Proxy11
|
||||
, proxy0, proxy1, proxy2, proxy3, proxy4, proxy5, proxy6, proxy7, proxy8, proxy9, proxy10, proxy11
|
||||
, class Tag0, class Tag1, class Tag2, class Tag3, class Tag4, class Tag5, class Tag6, class Tag7, class Tag8, class Tag9, class Tag10, class Tag11
|
||||
, tag0, tag1, tag2, tag3, tag4, tag5, tag6, tag7, tag8, tag9, tag10, tag11
|
||||
, ProxyT, proxyT
|
||||
, class TagT, tagT
|
||||
) where
|
||||
|
||||
import Control.Category (identity)
|
||||
@ -65,12 +63,12 @@ gcast a = m # map \f -> runLeibniz f a
|
||||
where
|
||||
m = eqT (typeRep :: _ a) (typeRep :: _ b)
|
||||
|
||||
gcast1 :: forall s t a c. Typeable a => Tag1 c => Tag1 s => Tag1 t => c (s a) -> Maybe (c (t a))
|
||||
gcast1 :: forall s t a c. Typeable a => TagT c => TagT s => TagT t => c (s a) -> Maybe (c (t a))
|
||||
gcast1 a = m # map \f -> runLeibniz f a
|
||||
where
|
||||
m = eqT (typeRep :: _ (s a)) (typeRep :: _ (t a))
|
||||
|
||||
gcast2 :: forall s t a b c. Typeable a => Typeable b => Tag1 c => Tag2 s => Tag2 t => c (s a b) -> Maybe (c (t a b))
|
||||
gcast2 :: forall s t a b c. Typeable a => Typeable b => TagT c => TagT s => TagT t => c (s a b) -> Maybe (c (t a b))
|
||||
gcast2 a = m # map \f -> runLeibniz f a
|
||||
where
|
||||
m = eqT (typeRep :: _ (s a b)) (typeRep :: _ (t a b))
|
||||
@ -94,101 +92,33 @@ unwrapSomeTypeRep (SomeTypeRep e) f = e # runExists f
|
||||
|
||||
-- MACHINERY + INSTANCES
|
||||
|
||||
foreign import typeRepDefault0 :: forall a. Tag0 a => TypeRep a
|
||||
foreign import typeRepFromTag1 :: forall a b. Tag1 a => Typeable b => TypeRep (a b)
|
||||
foreign import typeRepDefault0 :: forall a. TagT a => TypeRep a
|
||||
foreign import typeRepFromTag1 :: forall a b. TagT a => Typeable b => TypeRep (a b)
|
||||
foreign import showTypeRep :: forall a. TypeRep a -> String
|
||||
|
||||
-- Tagging types
|
||||
-- These would be a lot simpler after PolyKinds
|
||||
data Proxy0 (t :: Type)
|
||||
data Proxy1 (t :: Type -> Type)
|
||||
data Proxy2 (t :: Type -> Type -> Type)
|
||||
data Proxy3 (t :: Type -> Type -> Type -> Type)
|
||||
data Proxy4 (t :: Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy5 (t :: Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy6 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy7 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy8 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy9 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy10 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
data Proxy11 (t :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type)
|
||||
-- Tagging types, this is basically the same as `Type.Proxy`
|
||||
-- but we don't want to export any constructors
|
||||
data ProxyT :: forall k. k -> Type
|
||||
data ProxyT t
|
||||
|
||||
foreign import proxy0 :: forall t. Proxy0 t
|
||||
foreign import proxy1 :: forall t. Proxy1 t
|
||||
foreign import proxy2 :: forall t. Proxy2 t
|
||||
foreign import proxy3 :: forall t. Proxy3 t
|
||||
foreign import proxy4 :: forall t. Proxy4 t
|
||||
foreign import proxy5 :: forall t. Proxy5 t
|
||||
foreign import proxy6 :: forall t. Proxy6 t
|
||||
foreign import proxy7 :: forall t. Proxy7 t
|
||||
foreign import proxy8 :: forall t. Proxy8 t
|
||||
foreign import proxy9 :: forall t. Proxy9 t
|
||||
foreign import proxy10 :: forall t. Proxy10 t
|
||||
foreign import proxy11 :: forall t. Proxy11 t
|
||||
foreign import proxyT :: forall t. ProxyT t
|
||||
|
||||
class Tag0 a where tag0 :: Proxy0 a
|
||||
class Tag1 (a :: Type -> Type) where tag1 :: Proxy1 a
|
||||
class Tag2 (a :: Type -> Type -> Type) where tag2 :: Proxy2 a
|
||||
class Tag3 (a :: Type -> Type -> Type -> Type) where tag3 :: Proxy3 a
|
||||
class Tag4 (a :: Type -> Type -> Type -> Type -> Type) where tag4 :: Proxy4 a
|
||||
class Tag5 (a :: Type -> Type -> Type -> Type -> Type -> Type) where tag5 :: Proxy5 a
|
||||
class Tag6 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag6 :: Proxy6 a
|
||||
class Tag7 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag7 :: Proxy7 a
|
||||
class Tag8 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag8 :: Proxy8 a
|
||||
class Tag9 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag9 :: Proxy9 a
|
||||
class Tag10 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag10 :: Proxy10 a
|
||||
class Tag11 (a :: Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type -> Type) where tag11 :: Proxy11 a
|
||||
class TagT :: forall k. k -> Constraint
|
||||
class TagT a where tagT :: ProxyT a
|
||||
|
||||
-- foreign import proxy0FromTag1 :: forall t a. Tag1 t => Typeable a => Proxy0 (t a)
|
||||
foreign import proxy1FromTag2 :: forall t a. Tag2 t => Typeable a => Proxy1 (t a)
|
||||
foreign import proxy2FromTag3 :: forall t a. Tag3 t => Typeable a => Proxy2 (t a)
|
||||
foreign import proxy3FromTag4 :: forall t a. Tag4 t => Typeable a => Proxy3 (t a)
|
||||
foreign import proxy4FromTag5 :: forall t a. Tag5 t => Typeable a => Proxy4 (t a)
|
||||
foreign import proxy5FromTag6 :: forall t a. Tag6 t => Typeable a => Proxy5 (t a)
|
||||
foreign import proxy6FromTag7 :: forall t a. Tag7 t => Typeable a => Proxy6 (t a)
|
||||
foreign import proxy7FromTag8 :: forall t a. Tag8 t => Typeable a => Proxy7 (t a)
|
||||
foreign import proxy8FromTag9 :: forall t a. Tag9 t => Typeable a => Proxy8 (t a)
|
||||
foreign import proxy9FromTag10 :: forall t a. Tag10 t => Typeable a => Proxy9 (t a)
|
||||
foreign import proxy10FromTag11 :: forall t a. Tag11 t => Typeable a => Proxy10 (t a)
|
||||
foreign import proxyTFromTagT :: forall t a. TagT t => Typeable a => ProxyT (t a)
|
||||
|
||||
instance typeableRecord :: (RL.RowToList rs ls, TypeableRecordFields ls) => Typeable (Record rs) where
|
||||
typeRep = typeRowToTypeRep (typeableRecordFields (RLProxy :: _ ls))
|
||||
else
|
||||
instance tag0FromTag1 :: (Tag1 t, Typeable a) => Typeable (t a) where
|
||||
instance tagTFromTag1 :: (TagT t, Typeable a) => Typeable (t a) where
|
||||
typeRep = typeRepFromTag1
|
||||
else
|
||||
instance typeableTag0 :: Tag0 t => Typeable t where
|
||||
instance typeableTagT :: TagT t => Typeable t where
|
||||
typeRep = typeRepDefault0
|
||||
|
||||
instance tag1FromTag2 :: (Tag2 t, Typeable a) => Tag1 (t a) where
|
||||
tag1 = proxy1FromTag2
|
||||
|
||||
instance tag2FromTag3 :: (Tag3 t, Typeable a) => Tag2 (t a) where
|
||||
tag2 = proxy2FromTag3
|
||||
|
||||
instance tag3FromTag4 :: (Tag4 t, Typeable a) => Tag3 (t a) where
|
||||
tag3 = proxy3FromTag4
|
||||
|
||||
instance tag4FromTag5 :: (Tag5 t, Typeable a) => Tag4 (t a) where
|
||||
tag4 = proxy4FromTag5
|
||||
|
||||
instance tag5FromTag6 :: (Tag6 t, Typeable a) => Tag5 (t a) where
|
||||
tag5 = proxy5FromTag6
|
||||
|
||||
instance tag6FromTag7 :: (Tag7 t, Typeable a) => Tag6 (t a) where
|
||||
tag6 = proxy6FromTag7
|
||||
|
||||
instance tag7FromTag8 :: (Tag8 t, Typeable a) => Tag7 (t a) where
|
||||
tag7 = proxy7FromTag8
|
||||
|
||||
instance tag8FromTag9 :: (Tag9 t, Typeable a) => Tag8 (t a) where
|
||||
tag8 = proxy8FromTag9
|
||||
|
||||
instance tag9FromTag10 :: (Tag10 t, Typeable a) => Tag9 (t a) where
|
||||
tag9 = proxy9FromTag10
|
||||
|
||||
instance tag10FromTag11 :: (Tag11 t, Typeable a) => Tag10 (t a) where
|
||||
tag10 = proxy10FromTag11
|
||||
instance tagTFromTagT :: (TagT t, Typeable a) => TagT (t a) where
|
||||
tagT = proxyTFromTagT
|
||||
|
||||
-- COMMON INSTANCES
|
||||
|
||||
@ -220,35 +150,35 @@ instance typeableRecordFieldsCons
|
||||
key = SProxy :: _ key
|
||||
tail = typeableRecordFields (RLProxy :: _ rowlistTail)
|
||||
|
||||
instance taggedInt :: Tag0 Int where
|
||||
tag0 = proxy0
|
||||
instance taggedInt :: TagT Int where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0Boolean :: Tag0 Boolean where
|
||||
tag0 = proxy0
|
||||
instance tagTBoolean :: TagT Boolean where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0Number :: Tag0 Number where
|
||||
tag0 = proxy0
|
||||
instance tagTNumber :: TagT Number where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0Char :: Tag0 Char where
|
||||
tag0 = proxy0
|
||||
instance tagTChar :: TagT Char where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0String :: Tag0 String where
|
||||
tag0 = proxy0
|
||||
instance tagTString :: TagT String where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0Unit :: Tag0 Unit where
|
||||
tag0 = proxy0
|
||||
instance tagTUnit :: TagT Unit where
|
||||
tagT = proxyT
|
||||
|
||||
instance taggedArray :: Tag1 Array where
|
||||
tag1 = proxy1
|
||||
instance taggedArray :: TagT Array where
|
||||
tagT = proxyT
|
||||
|
||||
instance taggedMaybe :: Tag1 Maybe where
|
||||
tag1 = proxy1
|
||||
instance taggedMaybe :: TagT Maybe where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag2Func :: Tag2 (->) where
|
||||
tag2 = proxy2
|
||||
instance tag2Func :: TagT (->) where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag2Either :: Tag2 Either where
|
||||
tag2 = proxy2
|
||||
instance tag2Either :: TagT Either where
|
||||
tagT = proxyT
|
||||
|
||||
instance tag0Ordering :: Tag0 Ordering where
|
||||
tag0 = proxy0
|
||||
instance tagTOrdering :: TagT Ordering where
|
||||
tagT = proxyT
|
||||
|
||||
@ -3,26 +3,34 @@ module Test.Main where
|
||||
import Prelude
|
||||
|
||||
import Data.Either (Either)
|
||||
import Data.Typeable (class Tag0, class Tag1, class Tag3, TypeRep, eqTypeRep, proxy0, proxy1, proxy3, typeRep, typeRepFromVal)
|
||||
import Data.Typeable (class TagT, TypeRep, eqTypeRep, proxyT, typeRep, typeRepFromVal)
|
||||
import Effect (Effect)
|
||||
|
||||
foreign import clog :: forall a. a -> Effect Unit
|
||||
|
||||
main :: Effect Unit
|
||||
main = do
|
||||
clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Char))
|
||||
clog (eqTypeRep (typeRep :: _ Int) (typeRep :: _ Int))
|
||||
clog (typeRep :: _ Char)
|
||||
clog (typeRep :: _ Int)
|
||||
|
||||
clog (typeRep :: _ Array)
|
||||
clog (typeRep :: _ {name::String, age::Int})
|
||||
clog (eqTypeRep typeRecord (typeRep :: _ {name::String, age::Int}))
|
||||
clog (eqTypeRep (typeRep :: _ Person) typePerson)
|
||||
clog (eqTypeRep (typeRep :: _ (Array Person)) typeArrPerson)
|
||||
clog (eqTypeRep (typeRep :: _ (Array Person2)) typeArrPerson)
|
||||
clog (eqTypeRep (typeRep :: _ (Optional Int)) (typeRepFromVal (Some 1)))
|
||||
clog (eqTypeRep (typeRep :: _ (Optional Person)) (typeRepFromVal (Some 1)))
|
||||
clog (eqTypeRep (typeRep :: _ (Either Int Person)) (typeRep :: _ (Either Int Person)))
|
||||
clog (typeRep :: _ (Int -> Either (Either Int Int) (Optional (Array (Person)))))
|
||||
clog (typeRep :: _ (Either (Either Int Int) (Optional (Array (Person)))))
|
||||
clog (typeRep :: _ (Either Int Int))
|
||||
clog (typeRep :: _ Int)
|
||||
clog (typeRep :: _ (Foo Int Int Int))
|
||||
|
||||
clog (eqTypeRep (typeRep :: _ Array) (typeRep :: _ Array))
|
||||
clog (eqTypeRep (typeRep :: _ Person) typePerson)
|
||||
clog (eqTypeRep (typeRep :: _ (Array Person)) typeArrPerson)
|
||||
clog (eqTypeRep (typeRep :: _ (Array Person2)) typeArrPerson)
|
||||
clog (eqTypeRep typeRecord (typeRep :: _ {name::String, age::Int}))
|
||||
clog (eqTypeRep (typeRep :: _ (Optional Int)) (typeRepFromVal (Some 1)))
|
||||
clog (eqTypeRep (typeRep :: _ (Optional Person)) (typeRepFromVal (Some 1)))
|
||||
clog (eqTypeRep (typeRep :: _ (Either Int Person)) (typeRep :: _ (Either Int Person)))
|
||||
|
||||
where
|
||||
typeRecord :: TypeRep {age::Int, name::String}
|
||||
typeRecord = typeRep
|
||||
@ -37,14 +45,15 @@ main = do
|
||||
-- A data type without a typeable instance
|
||||
data Break
|
||||
|
||||
data Foo :: forall k1 k2 k3. k1 -> k2 -> k3 -> Type
|
||||
data Foo a b c = Foo
|
||||
instance tag3Foo :: Tag3 Foo where tag3 = proxy3
|
||||
instance tagFoo :: TagT Foo where tagT = proxyT
|
||||
|
||||
newtype Person = Person { name :: String, location :: String }
|
||||
instance tag0Person :: Tag0 Person where tag0 = proxy0
|
||||
instance tagTPerson :: TagT Person where tagT = proxyT
|
||||
|
||||
newtype Person2 = Person2 { name :: String, location :: String }
|
||||
instance tag0Person2 :: Tag0 Person2 where tag0 = proxy0
|
||||
instance tagTPerson2 :: TagT Person2 where tagT = proxyT
|
||||
|
||||
data Optional a = None | Some a
|
||||
instance tag1Optional :: Tag1 Optional where tag1 = proxy1
|
||||
instance tagOptional :: TagT Optional where tagT = proxyT
|
||||
|
||||
Loading…
Reference in New Issue
Block a user