A Quick and dirty start in idris: how to add arbitrary type restrictions in only 7 steps

Minimal type constraint in idris

I’ve been wanting to learn to use idris for a while, but the gamut of functional languages is pretty large right now. My daily driver is still F#, but I write an increasing amount of purescript for small problem solving … its runtime requirements are austere enough to run basically without support in a new, empty nashorn vm, which is quite impressive.

I’m always looking around to learn more, get even more formal, especially because I’m focused on code that will have a financial impact. I won’t be writing this one in idris, but I want to track it and have it as part of my toolbelt, should the inspiration to crank out (for example) a suitable DSL arise.

I won’t lie … I’m too dumb to understand proofs yet in idris. I wasn’t great at math in college after a certain point, and I tend to tie myself in circular knots writing proofs… It’s a skill though and I think I can improve with practice.

But what I want to talk about now is … ok I’m writing some idris … but … ok how does this help? I’m not smart enough to write real proofs.

Happily, there’s a simple pattern you can follow to pump up your type game without having to be smart. This is more like using constexpr computation in C++ template arguments than theorem proving, but it’s also in a natively functional language. Combining all this power leads to pretty neat things.

Step 1: Define a partial type ADT:

data IsEven : (b : Bool) -> Type where
  ItIsEven : IsEven True

We just need a type to carry around the Bool we’re interested in.

Step 2: Make the type uninhabited except where we want it

Uninhabited (IsEven False) where
  uninhabited IsEven impossible -- Cribbed from Nat.idr

Step 3: An ordinary function that evaluates the criterion:

itHasTheOneBitSet : (n : Nat) -> Bool
itHasTheOneBitSet Z = False
itHasTheOneBitSet (S Z) = True
itHasTheOneBitSet (S (S a)) = itHasTheOneBitSet a

Step 4: A function that turns it into a type (could be combined with 3, but it’s nice to have them separate).

itIsEven : (n : Nat) -> Type
itIsEven n =
  IsEven (not (itHasTheOneBitSet n))

Step 5: (using the Vect type from the docs), we can make a type that is only inhabited when what we want to have happen is happening (I think this is called an existential witness type). This record represents a higher standard of proof; that we have an even numbered vector:

record EvenVect (n : Nat) t where
 constructor MkEvenVect
 iseven : itIsEven n -- Type is inhabited only by ItIsEven
                     -- and specifically does not contain
                     -- IsEven False
 items : Vect n t

Step 6: Write the machinery that gets the job done: Being new to idris, there’s probably a way to get the size of the result vector to be assumed, but I’ve crudely computed it here.

div2 : Nat -> Nat
div2 Z = Z
div2 (S Z) = Z
div2 (S (S k)) = S (div2 k)
{- Type-unsafe map -}
map2unsafe : (t -> t -> u) -> Vect n t -> Vect (div2 n) u
map2unsafe f ((::@) a ((::@) b tail)) = (f a b) ::@ (map2unsafe f tail)
map2unsafe _ ((::@) _ VNil) = VNil
map2unsafe _ VNil = VNil

Step 7: Profit!

map2 : (t -> t -> u) -> EvenVect n t -> Vect (div2 n) u
map2 f v =
 map2unsafe f (items v)

Result:

mapped : Vect (S Z) String
mapped = 
 map2 
 (\a,b => a ++ b) 
 (MkEvenVect ItIsEven (“hi” ::@ “there” ::@ VNil))
{-
mappedNo : Vect (S Z) String
mappedNo = 
 map2 
 (\a,b => a ++ b) 
 (MkEvenVect ItIsEven (“hi” ::@ “there” ::@ “you” ::@ VNil))
- + Errors (1)
 `-- Minimal.idr line 52 col 5:
     When checking right hand side of mappedNo with expected type
             Vect 1 String
     
     When checking argument iseven to constructor Main.MkEvenVect:
             Type mismatch between
                     IsEven True (Type of ItIsEven)
             and
                     itIsEven 3 (Expected type)
             
             Specifically:
                     Type mismatch between
                             True
                     and
                             not (itHasTheOneBitSet 3)
-}
mappedYes : Vect (S (S Z)) String
mappedYes = 
 map2 
 (\a,b => a ++ b) 
 (MkEvenVect ItIsEven (“hi” ::@ “there” ::@ “you” ::@ “nerd” ::@ VNil))

:-)

I haven’t actually proved that map2unsafe requires pairs to take out of the vector, but I have constrained map2 to receive EvenVect which itself may only be constructed on even-length Vect. That’s what I wanted here, but the constraint is an arbitrary predicate. I wanted to get a start in idris to be able to do something even a bit practical with dependent types, but idris has a lot of ways of providing proofs, making types and type functions and doing just about anything, and a lot of it is daunting. I feel like I now have the ability to do somewhat interesting things within the bounds of what I’ve learned so far. Hopefully this helps others find their way and start constraining types with idris.