Last active
January 17, 2016 16:15
-
-
Save bishboria/72852a783d608c93b56d to your computer and use it in GitHub Desktop.
How do I fix the 'cannot decide' error in the opt function?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module LittleLang where | |
open import Data.Bool | |
open import Data.Nat | |
data type : Set where | |
tNat tBool : type | |
data exp : type → Set where | |
nat : ℕ → exp tNat | |
plus : exp tNat → exp tNat → exp tNat | |
bool : Bool → exp tBool | |
and : exp tBool → exp tBool → exp tBool | |
fromType : type → Set | |
fromType tNat = ℕ | |
fromType tBool = Bool | |
eval : ∀ {t : type} → exp t → fromType t | |
eval (nat n) = n | |
eval (plus n m) = eval n + eval m | |
eval (bool b) = b | |
eval (and a b) = eval a ∧ eval b | |
opt : ∀ {t : type} → exp t → exp t | |
opt (nat n) = nat n | |
opt (plus n m) with opt n | opt m | |
... | nat 0 | y = y | |
... | x | nat 0 = x | |
... | x | y = plus x y | |
opt (bool b) = bool b | |
opt (and a b) with opt a | opt b | |
... | bool true | y = y | |
... | x | bool true = x | |
... | x | y = and x y |
Thanks to @pigworker. I had to introduce a datatype to encode the types that LittleLang operates on and index exp
by that.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Even though there's no way to construct a
plus
term with typeexp Bool
, the compiler says it cannot decide if there should be a case for thebool
constructor. How do/Can I fix this?If I make the appropriate changes to accomodate
with eval n | eval m
everything type checks fine, but the program is essentially being fully evaluated (which isn't what I want).