Andy Matuschak on Twitter: "@raichoo @TacticalGrace Cool! Hm, help me understand: what are the dependent types buying you here?" / Twitter

I adore this extraordinarily beautiful implementation of arbitrary-dimensional, arbitrary-order bezier curves: github.com/hrldcpr/Bezier

3

7

23

.

I gave it a try and translated that into #idris using dependent types gist.github.com/raichoo/6020369

4

3

Replying to

Cool! Hm, help me understand: what are the dependent types buying you here?

Replying to

I took it as an exercise. Not sure if it makes sense to mix points of different dimensions here. I wanted bezier to be total

Replying to

gives you guarantee that the input and output dimensions are the same.

Conversation