lum/purescript-typeable
3
0
Fork 0
forked from github/purescript-typeable
Code Pull Requests Activity

A rewrite that's safer. Also add Dynamics.

Browse Source
This commit is contained in:
Anupam Jain 2021-01-11 03:16:31 +05:30
parent d68d3a6446
commit b390f684c7
9 changed files with 323 additions and 172 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

100
README.md
View File

@ -3,7 +3,7 @@ Reified types for Purescript
This is an implementation of indexed typereps for Purescript, similar to the [corresponding implementation in Haskell](https://hackage.haskell.org/package/base-4.10.0.0/docs/Type-Reflection.html#t:TypeRep).
## API
## Data.Typeable
`TypeReps` are values that represent types (i.e. they reify types). When they are *indexed* they have the type itself as a parameter.
@ -32,100 +32,56 @@ We can also test typereps for equality -
eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
```
## Mini tutorial on using Typeable and TypeReps
As an example, with typereps we can have dynamic values which carry around the type information as a value -
```purescript
data Dynamic' a = Dynamic' (TypeRep a) a
data Dynamic = Dynamic (Exists Dynamic')
-- Wrap a value into a dynamic
dynamic :: forall a.
dynamic a = Dynamic (mkExists (Dynamic' typeRep a)) -- The compiler picks the appropriate typerep automatically
```
To get a value out of a dynamic, we must have a way to convert a `TypeRep` into typelevel information. We do this with *witnesses*.
However witnesses require GADTs, and since Purescript does not have GADTs, we hack around it with Leibniz equality -
```purescript
-- | Two types are equal if they are _equal in all contexts_.
newtype Leibniz a b = Leibniz (forall f. f a -> f b)
infix 4 type Leibniz as ~
```
Now we can compare two typereps and recover type information -
We can compare two typeReps and extract a witness for type equality.
```purescript
eqT :: forall a b. TypeRep a -> TypeRep b -> Maybe (a ~ b)
eqT ta tb
| eqTypeRep ta tb = Just (unsafeCoerce identity)
| otherwise = Nothing
```
And use this information to unwrap a dynamic value. We need to pass the type we expect to find in the dynamic -
## Data.Dynamic
We can have dynamic values which holds a value `a` in a context `t` and forgets the type of `a`
```purescript
unwrapDynamic :: forall a. TypeRep a -> Dynamic -> Maybe a
unwrapDynamic ta (Dynamic e) = runExists e \(Dynamic ta tb) -> case eqT ta tb of
Nothing -> Nothing
Just witness -> runLeibniz witness tb
data Dynamic t
```
We can wrap a value into a dynamic
```purescript
-- Wrap a value into a dynamic
dynamic :: forall a t. Typeable a => t a -> Dynamic t
```
We can recover a value out of a dynamics if supply the type we expect to find in the Dynamic
```purescript
unwrapDynamic :: forall a. TypeRep a -> Dynamic t -> Maybe a
```
## Deriving `Typeable` for custom data types
### Create a `Tag` instance for your data type
It's extremely easy. You just need to create a mechanical `Tag` class instance for your datatype. There are different `Tag` classes for types of different arity.
First create a mechanical `Tag` class instance for your datatype. There are different `Tag` classes for types of different arity.
For example, to derive an instance for a plain data type, use `Tag1` and `Proxy1` -
For example, to derive an instance for a plain data type, use `Tag1` and `proxy1` -
```purescript
data Person = Person {name::String, age::Int}
instance tag1Person :: Tag1 Person where t1 = Proxy1
instance tag1Person :: Tag1 Person where t1 = proxy1
```
For a data type which takes one type parameter, use `Tag2` and `Proxy2`, and so on -
For a data type which takes one type parameter, use `Tag2` and `proxy2`, and so on -
```purescript
data Optional a = Some a | None
instance tag2Optional :: Tag2 Optional where t2 = Proxy2
instance tag2Optional :: Tag2 Optional where t2 = proxy2
```
Don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.
**Don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.**
> #### CAVEATS
> There are two cases where the compiler would not prevent you from writing an invalid instance. Without compiler support it's very hard to prevent these mistakes at compile time.
> However the good thing is that these mistakes are hard to make unless you are actively looking to subvert the type system, and accidental mistakes will be caught at compile time.
>
> 1. *Do not include type parameters in your instance*.
>
> For example do not create an instance for `Tag1 (Optional a)`.
>
> That would give the same typerep to all `Optional`s, for example `Optional Int` and `Optional String` would have the same typerep.
>
> The compiler would prevent you from including type params in your instance *accidentally*, for example you would get an error on defining an instance for `Tag2 (Optional a)`.
>
> 2. *Do not add any extra constraints to the instances*. For example don't do `Foo => Tag1 Person`.
> #### CAVEAT
> *Do not add any extra constraints to the instances*. For example don't do `Foo => Tag1 Person`. This currently cannot be caught by the type checker, but will break typerep comparisons for your data type.
### Then create a `Typeable` instance for your datatype
Write a mechanical `Typeable` instance for your datatype -
1. Use one of the baked in `typerepImpl` functions as the implementation for your instance. For example, use `typerepImpl1` for plain types which take no type arguments, use `typerepImpl2` for types that take one argument, and so on.
2. Add constrinats to make sure that all type parameters are `Typeable` too.
3. Add a constraint for appropriate tag instance as a constraint.
Again, don't worry about getting it wrong since the type system will prevent you from writing an invalid instance.
```purescript
instance typeablePerson :: Typeable Person where typeRep = typerepImpl1
```
```purescript
instance typeableOptional :: Typeable a => Typeable (Optional a) where typeRep = typerepImpl2
```
And that's it! You are done!
And that's it! You are done! Now your datatype will have a `Typeable` instance.

10
spago.dhall
View File

@ -3,7 +3,15 @@ Welcome to a Spago project!
You can edit this file as you like.
-}
{ name = "typeable"
, dependencies = [ "console", "effect", "psci-support", "either", "arrays" ]
, dependencies =
[ "console"
, "effect"
, "psci-support"
, "either"
, "arrays"
, "exists"
, "leibniz"
]
, packages = ./packages.dhall
, sources = [ "src/**/*.purs", "test/**/*.purs" ]
}

21
src/Data/Dynamic.purs Normal file
View 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)

64
src/Data/Typeable.js Normal file
View File

@ -0,0 +1,64 @@
exports.typeRepDefault0 = function(t) {
return t;
};
exports.typeRepFromTag1 = pack('tag1');
exports.showTypeRep = function(t) {
console.log(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;
// 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');
function pack(tagName) {
return function(origTag) {
let unwrappedTag = origTag[tagName];
return function(dict) {
if(unwrappedTag.tag) return {tag:unwrappedTag.tag, args:unwrappedTag.args.concat(dict)};
return {tag: origTag, args: [dict]};
};
};
};
exports.eqTypeRep = function(t1) {
return function(t2) {
return eqTypeRepHelper(t1,t2);
};
};
function eqTypeRepHelper(t1,t2) {
if(t1.tag0) return t1 === t2;
if(t1.tag !== t2.tag) return false;
if(t1.args.length !== t2.args.length) return false;
for (var i=0; i<t1.args.length;i++) {
if(!eqTypeRepHelper(t1.args[i].typeRep, t2.args[i].typeRep)) return false;
}
return true;
}

180
src/Data/Typeable.purs Normal file
View File

@ -0,0 +1,180 @@
module Data.Typeable
( TypeRep
, class Typeable
, typeRep
, eqT
, eqTypeRep
, typeRepFromVal
, SomeTypeRep(..)
, 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
) where
import Control.Category (identity)
import Data.Boolean (otherwise)
import Data.Either (Either)
import Data.Exists (Exists, runExists)
import Data.Function ((#))
import Data.Leibniz (type (~), Leibniz)
import Data.Maybe (Maybe(..))
import Data.Ordering (Ordering)
import Data.Show (class Show)
import Data.Unit (Unit)
import Unsafe.Coerce (unsafeCoerce)
-- | Indexed TypeReps
data TypeRep a
-- | `Typeable` things have a `TypeRep`
class Typeable a where
typeRep :: TypeRep a
instance showTypeRepInstance :: Show (TypeRep a) where
show t = showTypeRep t
-- | Compare two `TypeRep`, and potentially return a type witness for equality
eqT :: forall a b. TypeRep a -> TypeRep b -> Maybe (a ~ b)
eqT ta tb
| eqTypeRep ta tb = Just (unsafeCoerce (identity :: Leibniz a a))
| otherwise = Nothing
-- | Compare two `TypeRep`, potentially of differing types, for equality
foreign import eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
-- | Get the `TypeRep` for a value
typeRepFromVal :: forall a. Typeable a => a -> TypeRep a
typeRepFromVal _ = typeRep
-- | Unindexed typereps
data SomeTypeRep = SomeTypeRep (Exists TypeRep)
-- | Unwrap a TypeRep
unwrapSomeTypeRep :: forall r. SomeTypeRep -> (forall a. TypeRep a -> r) -> r
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 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)
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
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
-- 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)
instance tag0FromTag1 :: (Tag1 t, Typeable a) => Typeable (t a) where
typeRep = typeRepFromTag1
else
instance typeableTag0 :: Tag0 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
-- COMMON INSTANCES
instance taggedInt :: Tag0 Int where
tag0 = proxy0
instance tag0Boolean :: Tag0 Boolean where
tag0 = proxy0
instance tag0Number :: Tag0 Number where
tag0 = proxy0
instance tag0String :: Tag0 String where
tag0 = proxy0
instance tag0Unit :: Tag0 Unit where
tag0 = proxy0
instance taggedArray :: Tag1 Array where
tag1 = proxy1
instance tag2Func :: Tag2 (->) where
tag2 = proxy2
instance tag2Either :: Tag2 Either where
tag2 = proxy2
instance tag0Ordering :: Tag0 Ordering where
tag0 = proxy0

42
src/Typeable.js
View File

@ -1,42 +0,0 @@
exports.typerepImpl1 = function(t1) {
return t1;
};
exports.typerepImpl2 = function(t1) {
return function(t2) {
return [t1,t2];
};
};
exports.typerepImpl3 = function(t1) {
return function(t2) {
return function(t3) {
return [t1,t2,t3];
};
};
};
exports.eqTypeRep = function(t1) {
return function(t2) {
return nestedArrayEq(t1, t2);
};
};
exports.clog = function(a) {
return function() {
console.log("CLOG:", a);
};
};
function nestedArrayEq(t1, t2) {
if(Array.isArray(t1)) {
if(!(Array.isArray(t2) && (t1.length == t2.length)))
return false;
for (var i=0; i<t1.length;i++) {
if(!nestedArrayEq(t1[i], t2[i]))
return false;
}
return true;
}
return t1 === t2;
}

40
src/Typeable.purs
View File

@ -1,40 +0,0 @@
module Typeable where
import Data.Either (Either)
import Data.Unit (Unit)
import Effect (Effect)
-- Indexed TypeReps
data TypeRep a
-- Typeable class
class Typeable a where
typeRep :: TypeRep a
-- Implementation detail
-- Tagging types
data Proxy1 a = Proxy1
data Proxy2 (t :: Type -> Type) = Proxy2
data Proxy3 (t :: Type -> Type -> Type) = Proxy3
class Tag1 a where t1 :: Proxy1 a
class Tag2 (a :: Type -> Type) where t2 :: Proxy2 a
class Tag3 (a :: Type -> Type -> Type) where t3 :: Proxy3 a
-- Constructors for the opaque data type
foreign import typerepImpl1 :: forall a. Tag1 a => TypeRep a
foreign import typerepImpl2 :: forall a b. Tag2 a => Typeable b => TypeRep (a b)
foreign import typerepImpl3 :: forall a b c. Tag3 a => Typeable b => Typeable c => TypeRep (a b c)
-- Type equality
foreign import eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean
-- Common instances
instance tag1Int :: Tag1 Int where t1 = Proxy1
instance typeableInt :: Typeable Int where typeRep = typerepImpl1
instance tag2Array :: Tag2 Array where t2 = Proxy2
instance typeableArray :: Typeable a => Typeable (Array a) where typeRep = typerepImpl2
instance tag3Either :: Tag3 Either where t3 = Proxy3
instance typeableEither :: (Typeable a, Typeable b) => Typeable (Either a b) where typeRep = typerepImpl3
-- DEBUG: Console.log anything
foreign import clog :: forall a. a -> Effect Unit

5
test/Main.js Normal file
View File

@ -0,0 +1,5 @@
exports.clog = function(x) {
return function() {
console.log(x);
};
};

33
test/Main.purs
View File

@ -3,39 +3,38 @@ 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 Effect (Effect)
import Typeable (class Tag1, class Tag2, class Typeable, Proxy1(..), Proxy2(..), TypeRep, clog, eqTypeRep, typeRep, typerepImpl1, typerepImpl2)
foreign import clog :: forall a. a -> Effect Unit
main :: Effect Unit
main = do
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 :: _ (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))
where
typeArrPerson :: TypeRep (Array Person)
typeArrPerson = typeRep
typePerson :: TypeRep Person
typePerson = typeRep
data Foo a b c = Foo
instance tag3Foo :: Tag3 Foo where tag3 = proxy3
newtype Person = Person { name :: String, location :: String }
instance tag0Person :: Tag0 Person where tag0 = proxy0
newtype Person2 = Person2 { name :: String, location :: String }
-- Create Typeable instances for Person
instance tag1Person :: Tag1 Person where t1 = Proxy1
instance typeablePerson :: Typeable Person where typeRep = typerepImpl1
-- Create Typeable instances for Person2
instance tag1Person2 :: Tag1 Person2 where t1 = Proxy1
instance typeablePerson2 :: Typeable Person2 where typeRep = typerepImpl1
instance tag0Person2 :: Tag0 Person2 where tag0 = proxy0
data Optional a = None | Some a
-- Create Typeable instances for Person
instance tag2Optional :: Tag2 Optional where t2 = Proxy2
instance typeableOptional :: Typeable a => Typeable (Optional a) where
typeRep = typerepImpl2
typeRepFromVal :: forall a. Typeable a => a -> TypeRep a
typeRepFromVal _ = typeRep
instance tag1Optional :: Tag1 Optional where tag1 = proxy1