Idris version of https://github.com/hrldcpr/Bezier.hs/blob/master/Bezier.hs

bezier.hs

module Bezier

Point : Type -> Nat -> Type
Point = Vect  

-- parametric line between two points:
line : Num a => Point a d -> Point a d -> a -> Point a d
line p q t = zipWith interpolate p q
  where interpolate a b = (1 - t)*a + t*b

-- bezier of just one point is fixed at that point,
-- and bezier of a list of points is just linear interpolation
-- between bezier of the initial part of the list
-- and bezier of the tail of the list:
bezier : Num a => Vect (Point a d) (S n) -> a -> Point a d
bezier (p  :: Nil)       t = p
bezier (p1 :: p2 :: ps)  t =
  let points = (p1 :: p2 :: ps) in
    line (bezier (init points) t) (bezier (tail points) t) t