0
$\begingroup$

In the companion code to A Tutorial Implementation of a Dependently Typed Lambda Calculus - prelude.lp - there is a rather intimidating definition of a boolElim function that's not described in the paper itself:

let boolElim =
  ( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *)
                                    (\ _ -> Unit) (\ _ -> Unit)
                                    (\ x -> m x)
                                    (\ _ _ _ -> Unit) )
                         ( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *)
                                                      (\ _ -> Unit)
                                                      (\ x -> m x)
                                                      (\ _ _ _ -> Unit)
                                                      n (FZero n))
                                    U mf (\ _ _ -> U) )
                         ( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *)
                                                                  (\ _ -> Unit)
                                                                  (\ x -> m x)
                                                                  (\ _ _ _ -> Unit)
                                                                  n (FSucc n f) )
                                              ( natElim
                                                  ( \ n -> natElim
                                                             (\ n -> Fin (Succ (Succ n)) -> *)
                                                             (\ x -> m x)
                                                             (\ _ _ _ -> Unit)
                                                             n (FSucc (Succ n) (FZero n)) )
                                                  mt (\ _ _ -> U) )
                                              ( \ n f _ -> finElim
                                                             (\ n f -> natElim
                                                                         (\ n -> Fin (Succ (Succ n)) -> *)
                                                                         (\ x -> m x)
                                                                         (\ _ _ _ -> Unit)
                                                                         n (FSucc (Succ n) (FSucc n f)))
                                                             (\ _ -> U)
                                                             (\ _ _ _ -> U)
                                                             n f )
                                              n f )
                         2 )
  :: forall (m :: Bool -> *) . m False -> m True -> forall (b :: Bool) . m b

The type indicates its behaviour (an if-else), but I can't make any headway with the definition. Can someone break it down for me?

$\endgroup$
  • $\begingroup$ I think the code is a bit long to ask about in a stackexchange post. Is there a way to shorten the code to just the part you don't get? $\endgroup$ – 6005 May 14 at 12:41
  • $\begingroup$ @6005 I don't really get any of it $\endgroup$ – Matt R May 14 at 15:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.