Home Reading Searching Subscribe Sponsors Statistics Posting Contact Spam Lists Links About Hosting Filtering Features Download Marketing Archives FAQ Blog From: Konstantin Tretjakov public.gmane.org> Subject: Question regarding a simple "dependently typed IF-THEN-ELSE" Newsgroups: gmane.comp.lang.agda Date: Monday 10th March 2014 15:54:12 UTC (over 4 years ago) ```Hello, suppose I would like to be able to use if-then-else in something like the following: f t = if t then true else zero My current attempt at doing it (Agda 2.3.0.1, Windows) is this: -------------------------------- module Test1 where postulate Level : Set lze : Level lsu : Level -> Level lmax : Level -> Level -> Level {-# BUILTIN LEVEL Level #-} {-# BUILTIN LEVELZERO lze #-} {-# BUILTIN LEVELSUC lsu #-} {-# BUILTIN LEVELMAX lmax #-} data Bool : Set where true false : Bool data ℕ : Set where zero : ℕ suc : ℕ → ℕ {- Set level of the return type of the if-then-else operator -} if[Level]_then_else_ : Bool → Level → Level → Level if[Level] true then x else y = x if[Level] false then x else y = y {- Return type of the if-then-else operator -} if[Set*]_then_else_ : ∀ {i j} (t : Bool) → Set i → Set j → Set (if[Level] t then i else j) if[Set*] true then A else B = A if[Set*] false then A else B = B {- Define the actual if-then-else operator -} if_then_else_ : ∀ {i j}{A : Set i}{B : Set j}(t : Bool) → A → B → (if[Set*] t then A else B) if true then x else y = x if false then x else y = y {- The test -} f : (t : Bool) → if[Set*] t then Bool else ℕ f t = if t then true else zero -------------------------------- This seems to work fine. However, the version, where I use the "most general" if_then_else_ in the type declaration, i.e.: f : (t : Bool) → if t then Bool else ℕ f t = if t then true else zero would not go through, reporting that: if[Set*] t then Set else Set !=< Set (_53 t) of type Set (if[Level] t then lsu lze else lsu lze) when checking that the expression if t then Bool else ℕ has type Set (_53 t) I do not understand the reason for this behaviour. Is it a bug of the version I am using, or am I misunderstanding something here? After all, simply writing g1 : Set g1 = if[Set*] true then Bool else ℕ g2 : Set g2 = if true then Bool else ℕ seems to work totally fine. Thank you, K. PS: A couple of optional noob questions, once I'm at it: * Is it possible to somehow verify that g1 == g2 in the last code snippet above? * Is there a possibility to do pattern-matching on type expressions in Agda? (e.g. f: (t = true) → ... f: (t = false) → ...)```
CD: 17ms