Reified types for Purescript
Go to file
2021-01-21 16:19:38 +05:30
src/Data Add more instances 2021-01-21 16:19:38 +05:30
test Add Typeable instances for records 2021-01-12 01:34:12 +05:30
.gitignore Init 2021-01-06 10:34:30 +05:30
package.json Init 2021-01-06 10:34:30 +05:30
packages.dhall Init 2021-01-06 10:34:30 +05:30
pnpm-lock.yaml Init 2021-01-06 10:34:30 +05:30
README.md Add link to slides for the talk 2021-01-18 11:30:44 +00:00
spago.dhall Add cast, gcast1, gcast2 2021-01-13 14:21:57 +05:30

Purescript-Typeable

Reified types for Purescript

This is an implementation of indexed typereps for Purescript, similar to the corresponding implementation in Haskell.

Slides for a talk about Purescript-Typeable, presented at the Purescript semi-monthly meetup on 18 January 2021, are available.

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.

data TypeRep a -- A *value* that represents the type 'a'

All typeable things have typereps -

class Typeable a where
  typeRep :: TypeRep a

Instances are provided for common data types.

We can recover the unindexed representation by making it existential -

data SomeTypeRep = SomeTypeRep (Exists TypeRep)

We can also test typereps for equality -

eqTypeRep :: forall a b. TypeRep a -> TypeRep b -> Boolean

We can compare two typeReps and extract a witness for type equality.

eqT :: forall a b. TypeRep a -> TypeRep b -> Maybe (a ~ b)

Data.Dynamic

We can have dynamic values which holds a value a in a context t and forgets the type of a

data Dynamic t

We can wrap a value into a dynamic

-- 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

unwrapDynamic :: forall a. TypeRep a -> Dynamic t -> Maybe a

Deriving Typeable for custom data types

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.

For example, to derive an instance for a plain data type, use Tag1 and proxy1 -

data Person = Person {name::String, age::Int}

instance tag1Person :: Tag1 Person where t1 = proxy1

For a data type which takes one type parameter, use Tag2 and proxy2, and so on -

data Optional a = Some a | None

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.

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.

And that's it! You are done! Now your datatype will have a Typeable instance.