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).
Subscribe to:
Posts (Atom)