A question regarding type safety of generated code

[oco-adam]

Hi @bamboo,

I'm new to Idris and was playing around with your code generator, seeing if it might be possible to generate dart library code:

I see that in the generated code, all generated dart types are dynamic, and in particular, primitive type information is lost. I was wondering if you could please explain why you implemented this way?

I realise that there will be many Idris types which cannot be canonically expressed in dart types, but for primitive types, might it be possible to map them to corresponding dart types? The aim would be to generate dart library code with more type information, so that e.g. the generated dart functions maintained some level of type safety.

This is probably more of a quest to try and understand things better myself rather than a feature request, however I would eventually be willing to help out if you thought this kind of thing would be possible/useful.

[bamboo]

Hi @oco-adam,

I see that in the generated code, all generated dart types are dynamic, and in particular, primitive type information is lost. I was wondering if you could please explain why you implemented this way?

It was the quickest mapping from the chosen untyped intermediate representation produced by Idris to Dart code but my goal is to produce better and more strongly typed Dart code. Towards that goal I'm currently investigating the idea of introducing a typed IR closer to Dart which would allow for a type reconstruction algorithm to be run before emitting the actual Dart code.

I would eventually be willing to help out if you thought this kind of thing would be possible/useful.

Yes, that would be great.

[aeiou-st]

primitive type information is lost