2009 - Idris

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