Purescript-Typeable

[ajnsit]

I was looking for a Typeable implementation for Purescript and found this repo (https://github.com/joneshf/purescript-typeable) but -

1. The repo looks abandoned.
2. The typereps are unindexed.
3. There is nothing stopping people from implementing typereps “wrong” for custom types.

Also, from this discussion it looks like there is no plan yet for adding compiler support for Typeable in Purescript

So to scratch my own itch, I hacked together something with FFI - https://github.com/ajnsit/purescript-typeable. It provides a Typeable typeclass and allows writing mechanical instances for custom datatypes which are impossible to get wrong. It also provides an eqTypeRep :: TypeRep a -> TypeRep b -> Boolean function.

This is still very crude but I just wanted to get feedback first. Is there a better way to do this?

[paluh]

This is interesting. Thanks for sharing!

I’ve never used Typeable as I’m not a Haskeller (I’ve tried, but you know… I’ve found PureScript ;-))… Do you think that I can use any Haskell based intro (like this) to understand your new lib?

P.S. A quick intro about the lib usage and internals for PureScripters on some future meetup would be really cool

[jy14898]

If I understand how this has been implemented, it is essentially using the dictionary for the type class as a unique identifier at runtime to allow checking of which PS type a value came from? If so, that’s very clever, however it seems like derive newtype instance-based dictionaries would allow a way to break this approach?

[ntwilson]

You’ve probably seen this already, but it seems worthwhile to link to the earlier discussion on typeable:

Alternative to Typeable in PureScript

Hi all, I’ve a question about the status of Typeable in PureScript. What I like to do is check at runtime that the type of a container I have and the type of input from the user are equal. A simplified version in Haskell using GADTs where the type a in Input is existential: data Container :: Type -> Type where Elem :: Typeable a => a -> Container a -- more omitted -- data Input :: Type where Change :: Typeable a => a -> Input -- more omitted -- During runtime using eqT and :~:: han…

[natefaubion]

One issue with using dictionary equality is that the compiler does not guarantee any sort of referential stability. For dictionaries that require other dictionaries, these are unlikely to be stable over the entire program.

[ajnsit]

@paluh

Do you think that I can use any Haskell based intro (like this ) to understand your new lib?

That tutorial seems geared towards explaining the typerep-map library which is another thing on top of typereps. Unfortunately I don’t have a good resource on typereps handy, I’ll post it here when I find one.

@paluh

P.S. A quick intro about the lib usage and internals for PureScripters on some future meetup would be really cool

I’ll be happy to! The next meetup is also at a more convenient hour for me!

@jy14898

If I understand how this has been implemented, it is essentially using the dictionary for the type class as a unique identifier at runtime to allow checking of which PS type a value came from?

Yes! Since the typeclasses are automatically generated, there’s no way for the user to write an invalid or conflicting instance of Typeable.

@jy14898

however it seems like derive newtype instance-based dictionaries would allow a way to break this approach?

Not sure, I will have to look at how those are generated.

@ntwilson

You’ve probably seen this already, but it seems worthwhile to link to the earlier discussion on typeable:

Yup I saw this but that approach is inherently unsafe because the user can create arbitrary typeable instances.

@natefaubion

One issue with using dictionary equality is that the compiler does not guarantee any sort of referential stability. For dictionaries that require other dictionaries, these are unlikely to be stable over the entire program.

This solution only needs the “leaf” level dictionaries to be stable (i.e. allow pointer equality). The code already handles dictionaries that require other dictionaries, for example Typeable a => Typeable (t a), by comparing structurally instead.

[natefaubion]

@ajnsit

This solution only needs the “leaf” level dictionaries to be stable (i.e. allow pointer equality). The code already handles dictionaries that require other dictionaries, for example Typeable a => Typeable (t a), by comparing structurally instead.

I see, you are using a Tag instance as a stable referential identifier. Very clever indeed!

[natefaubion]

@ajnsit

Yup I saw this but that approach is inherently unsafe because the user can create arbitrary typeable instances.

This approach is still a bit unsafe, FWIW, because there isn’t anything disallowing a Tag instance from taking other dictionaries, but it’s definitely better than arbitrary string munging.

[natefaubion]

Can you derive an instance for Record? I suspect you’d want something like nested [key, dict] pairs.

[ajnsit]

@natefaubion

This approach is still a bit unsafe, FWIW, because there isn’t anything disallowing a Tag instance from taking other dictionaries

Ah good point!

I guess the saving grace is that the user can only break their own custom types. There’s no way to construct a typerep that conflicts with another typerep.

@natefaubion

Can you derive an instance for Record? I suspect you’d want something like nested [key, dict] pairs.

Yes I imagine it’ll require introducing Array (Tuple key dict).

How do you derive instances for Records in Purescript? I guess it will require compiler support?

[natefaubion]

@ajnsit

How do you derive instances for Records in Purescript? I guess it will require compiler support?

You would construct a TypeRep inductively via RowList and RowToList. There are examples in Prelude for things like Show, Eq, Ord, etc.

@ajnsit

I guess the saving grace is that the user can only break their own custom types. There’s no way to construct a typerep that conflicts with another typerep.

Good point. I guess you would only be able to construct something that creates false negatives (TypeReps are never equal), rather than construct something that allows you to coerce to a different type.

[ajnsit]

@natefaubion

You would construct a TypeRep inductively via RowList and RowToList. There are examples in Prelude for things like Show, Eq, Ord, etc.

Thanks! I added this.

I also made it quite a bit safer and less tedious. Now you only need to derive a tag instance (which is hard to mess up) and the typeable instance is auto derived.

[timjs]

I indeed played with it some time ago. Never published my findings however, used Haskell and Idris in the end to write a solution.

I managed to derive a TypeRep (I called it a Reflection) using PureScript generics mechanism. It kind of “saves” the generic representation of a type. I used it to implement a Dynamic data type (which I called Anything). I pushed it in the repo purescript-type-reflection, so you can take a look.

Can’t recall exactly what my problems were with this implementation at that time, but I think it was not possible to calculate the reflection of a recursive data type (see the Tree and List examples in Main)…

Seems like you managed to implement Typeable in a more performant way using the dict-trick!

[ajnsit]

@timjs

I managed to derive a TypeRep (I called it a Reflection) using PureScript generics mechanism. It kind of “saves” the generic representation of a type.

Ah I considered using generics for this, as generics is the closest we have to compiler assisted derivation in Purescript. However, the problem is that generics rely on the compiler retaining the type information. So generics can be used to distinguish between the variants of a particular data type, but not to distinguish between two separate data types. So retaining type information when going from Type -> Value -> Type is not possible and that AFAIK makes it impossible to create a proper Typeable instance.

For example, I don’t think it’s possible to use generics to generate different typereps for these two data types -

data Bool = True | False
data Foo = Bar | Baz

Perhaps some combination of generics and (ab)using dictionaries like my solution might work?

[hdgarrood]

Generics can distinguish those, as constructor names are present in the generic representation types: they’re the first type argument of Constructor. However, there are still problems with using Generic to generate Typeable typereps: firstly, the name of the type itself is not present in the representation type, and neither is the module in which it is defined. Secondly, all types ought to be able to be given Typeable instances, but many types should not have Generic instances - in particular, those whose constructors are not exported.