Why Idris don't have guards?

[Corvo Liu]

Dear all, 

  I'm trying Idris these days, I've found that there's no guards for Idris. Is there a specific reason why we don't have guards? 

Thanks a lot! 

Corvo 

[Jan de Muijnck-Hughes]

Hi Corvo;

While Idris doesn't support guards as one would find in Haskell, Idris does support a more generic construct: Views and Covering functions. This construct makes use of dependent types to construct views over your data that you can pattern match on.

For example, consider the following trivial haskell function which returns true if `x` is greater than twenty.

```

above20 :: Int -> Bool
above20 x | x > 20 = True
          | otherwise = False

```

Guards are used to compare x against the value twenty.

In Idris we can do something similar.

First we construct a 'view' describing what we want, which in this case is that the given value is greater than twenty.

```

data Above20 : (x : Nat) -> Type where
  IsAbove : GT x 20 -> Above20 x
  IsNot   : (GT x 20 -> Void) -> Above20 x
```

Our view has two viewpoints: 1) there is a predicate (a data type that holds some truth) stating that the value is greater than twenty; and 2) there is proof (by contradiction) that x is not greater than twenty.

With this view we can then construct a 'covering' function to compute the view. Convention means we name the view and covering function the same.

```

above20 : (x : Nat) -> Above20 x
above20 x with (isGT x 20)
  above20 x | (Yes prf) = IsAbove prf
  above20 x | (No contra) = IsNot contra

```

Here we have used dependent pattern matching (`with`) together with the function (`isGT`) that computes the evidence that x is either greater than twenty or not.

Putting it all together we can use the view to help with the pattern matching.

```

isAbove20 : (x : Nat) -> Bool
isAbove20 x with (above20 x)
  isAbove20 x | (IsAbove y) = True
  isAbove20 x | (IsNot f) = False

```

Notice that an even better way to write this function would be to skip the views and use the predicate directly, but then one wouldn't see the power of Views. We can use them to influence pattern matching by describing our cases using the views. One can do the same with predicates.

Whilst Views & Covering Functions are not the same as Guards, I have found that there is enough overlap that I do not miss not using guards. TBH I seldom used guards in Haskell in the first instance. But that last thing says more about me than anything else.

Regardless, you can find more information in the documentation about Views and Covering Functions [1]. They are a really powerful idiom that helps us to write our programs with greater accuracy. Predicates to for that matter!

[1] https://idris2.readthedocs.io/en/latest/tutorial/views.html

Hope this helps.

Jan

PS IMHO the difference between predicates and views are that predicates are a decidable test, and views *should* but don't need to describe all angles.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/idris-lang/0babc00d-7244-4e1e-9b5e-e239084b350dn%40googlegroups.com.

[Corvo Liu]

Wow! Thanks a lot! This really helps

Corvo 

[alru...@gmail.com]

Not to detract from the cool dependent-type stuff you can do with views, but the with syntax will let you play in ye olde not-dependent-type world like it's just a guard, too.

above20: Int -> Bool            
above20 x with (x > 20)         
   above20 _ | True = True      
   above20 _ | otherwise = False