Saturday, 9 January 2016


Idris Adventures - a nice surprise.

Let's compare 3 examples.

The following code compiles:

Example 1:

data D :Nat-> Type where
  MkD:  (a:Nat)->  D a

showNat : (D a)->String
showNat (MkD a) =show a

but the following does NOT compile:

Example 2:


data D :Nat-> Type where
  MkD:  (a:Nat)->  D a

showNat : (D a)->String
showNat (MkD b) =show b

why not ?

Because the following DOES compile:

Example 3:

data D :Nat-> Type where
  MkD:  (a:Nat)->  D Z

showNat : (D a)->String
showNat (MkD c) =show c

Why does Example 1 and 3 compile and 2 not ?

Because Idris knows in Example 2 that the parameter a is the same in the type and in the value because of  the constraint given by the data constructor MkD: (a:Nat)-> D a .


Cool !

--

UPDATE:

Perhaps this is a bug.... - to be confirmed.

because this :

showD : D a -> String; 
showD {a = x} (MkD x) = show x


compiles too.

The { } means pattern match. It brings a into scope, from the type level to the value level and then assigns a to x (yes, that is a reverse assignment syntax).