News for hackers. Stuff that matters.

A comment on Idris: A Language for Type-Driven Development. Parent comment

Re:Idris: A Language for Type-Driven Development by kitd on Friday January 20, 2023 @11:40AM (#34455632)
This is presumably not what you're thinking of but ofc Javascript uses objects as prototype "types". As is, they wont provide what you want, but if there was some kind of "compile-time" processing of prototypes such that types assemblies, dependencies, constraints and other relationships could be manipulated or asserted before they were applied in runtime code, that may provide some of the "first-class type" functionality mentioned.

Ed: actually, Typescript might be a better host for this.

[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by eckza on Friday January 20, 2023 @01:58PM (#34457948)
FP Or Die Gang is downvoting you, but this is actually correct.

No referential transparency (among other things, no doubt) makes this a harder problem to solve than just using a language that supports it.

$0.02

[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by still_grokking on Saturday January 21, 2023 @05:57AM (#34465539)
If you don't have referential transparency mathematical equations don't hold. You can't be sure that `a = b` stays true if deducted once.

So "the problem" doesn't get only harder, it becomes impossible to solve in a formal way.

[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by eckza on Wednesday January 25, 2023 @07:59PM (#34526443)
Thank you for this. That's exactly what I was getting at; you illustrated it far better.
[ Parent | on HN ]
Re:Idris: A Language for Type-Driven Development by still_grokking on Saturday January 21, 2023 @06:01AM (#34465559)
The down-votes are likely because the example isn't anyhow good.

But the idea to have static prototype types is imho quite interesting on its own. I was thinking a lot about that in the past.

I would love to have JS like objects—but in a static context.

Row polymorphism and extensible records are close but still not there actually.

[ Parent | on HN ]