Idris: A Language for Type-Driven Development

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 ]