#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
||| Type signatures
inN : Fin n -> Fin n -> Bool
genN : Vect n (Vect n Char)
inN {n=S _} x y = x==0 || x==y || x==last
genN = [[ if inN x y then 'N' else ' ' | x<-range ]| y<-range ]
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