Part2_Sec4_2_2_gen

Markdown generated from:
Source idr program: /src/Part2/Sec4_2_2_gen.idr
Source lhs program: /src/Part2/Sec4_2_2_gen.lhs

Section 4.2.2. More of Idris amazing code synthesis abilities vs Haskell

Idris code example

{-
Couple of interesting cases where Idris code generation just shines
-}
module Part2.Sec4_2_2_gen
import Data.Vect

{-
2 case splits and Idris solution search works!
-}
zipV : Vect n a -> Vect n b -> Vect n (a,b)
zipV [] [] = [] 
-- note this would also work (Idris, you figure it out!)
-- zipV [] _ = []
zipV (x :: xs) (y :: ys) = (x, y) :: zipV xs ys

{-
Bonus case follows the rules above
-}
zipWithV : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c 
zipWithV f [] [] = []
zipWithV f (x :: xs) (y :: ys) = f x y :: zipWithV f xs ys

{-
  This is again simple case split on the first variable and Idris finds solutions
-}
appendV : Vect n a -> Vect m a -> Vect (n + m) a  
appendV [] ys = ys
appendV (x :: xs) ys = x :: appendV xs ys

Idris wrote all this code after some case splits.

Compared to Haskell

module Part2.Sec4_2_2_gen where

As far as code generation goes, I think Haskell cannot compare here.