# 2009 - [Idris](http://www.idris-lang.org/)

Idris is a dependantly-typed, pure functional language that emphasises being in fact practically usable for real-world applications, apart from offering the extremely rigorous proof possibilities that are achievable with dependant types.

Task 1
---

    module Main
    
    main : IO ()
    main = putStrLn "Idris was made in 2009!"

Task 2
---

    module InN
    
    import Data.Fin
    import Data.Vect
    
    genN : Vect n (Vect n Char)
    genN = [[ if inN x y then 'N' else ' ' | x<-range ]| y<-range ]

    ||| Helper function, determines whether the char at coordinate (x,y)
    ||| is part of the letter:
    inN : Fin n -> Fin n -> Bool
    inN {n=S _} x y = x==0 || x==y || x==last
    

This one is not a program but just a function (more precisely, _dependant value_), producing the desired letter N as a two-dimensional array.

    $ idris ascii-n.idr 
         ____    __     _                                          
        /  _/___/ /____(_)____                                     
        / // __  / ___/ / ___/     Version 0.9.17.1-
      _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
     /___/\__,_/_/  /_/____/       Type :? for help               
    
    Idris is free software with ABSOLUTELY NO WARRANTY.            
    For details type :warranty.
    Type checking ./ascii-n.idr
    *ascii-n> genN {n=4}
    [['N', ' ', ' ', 'N'],
     ['N', 'N', ' ', 'N'],
     ['N', ' ', 'N', 'N'],
     ['N', ' ', ' ', 'N']] : Vect 4 (Vect 4 Char)


Task 3
---

    module gcd
    
    gcd' : Nat -> Nat -> Nat
    gcd' a Z = a
    gcd' a b = gcd' b $ a`mod`b

Note that I had to choose the name `gcd'` because as `gcd` it is already defined in the Idris prelude.

    Type checking ./gcd.idr
    *gcd> gcd' 8 12
    4 : Nat
    *gcd> gcd' 12 8
    4 : Nat
    *gcd> gcd' 234 876
    6 : Nat