# 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) -> BoolitHasTheOneBitSet Z = FalseitHasTheOneBitSet (S Z) = TrueitHasTheOneBitSet (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) -> TypeitIsEven 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 -> Natdiv2 Z = Zdiv2 (S Z) = Zdiv2 (S (S k)) = S (div2 k){- Type-unsafe map -}map2unsafe : (t -> t -> u) -> Vect n t -> Vect (div2 n) umap2unsafe f ((::@) a ((::@) b tail)) = (f a b) ::@ (map2unsafe f tail)map2unsafe _ ((::@) _ VNil) = VNilmap2unsafe _ VNil = VNil`

Step 7: Profit!

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

Result:

`mapped : Vect (S Z) Stringmapped =  map2  (\a,b => a ++ b)  (MkEvenVect ItIsEven (“hi” ::@ “there” ::@ VNil)){-mappedNo : Vect (S Z) StringmappedNo =  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)) StringmappedYes =  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.