3 ms·

Wouldn't the proposed function then just not compile for the instances were it would be impossible to test, as desired? It would still be useful for where it d

• tel 12y ago
  You can sort of do this sometimes. Consider Idris' decidable equality module: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Decidable/Equality.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/pre... Idris has type classes and it produces a polymorphic total function `decEq` for any type which instantiates the class DecEq. decEq :: DecEq t => (x : t) -> y -> Dec (x = y) where Dec denotes a decidable type, something like (but not actually) data Dec t where Yes : t -> Dec t No : Not t -> Dec t So now we have a proposition in our type-level prolog called `DecEq` and some types, the ones with decidable equality, can instantiate it instance DecEq () where decEq _ _ = Yes refl -- Equality is symmetric, so is the negation of equality total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_) negEqSym p h = p (sym h) -- Proof that zero isn't equal to any number greater than zero total OnotS : Z = S n -> _|_ OnotS refl impossible instance DecEq Nat where decEq Z Z = Yes refl decEq Z (S _) = No OnotS decEq (S _) Z = No (negEqSym OnotS) -- recurse on the arguments together and modify the eventual -- decided proof so as to match the arguments actually passed. -- -- I.e. we might find that Yes (n = m) but we need Yes (S n = S m) -- decEq (S n) (S m) with (decEq n m) | Yes p = Yes $ cong p | No p = No $ \h : (S n = S m) => p $ succInjective n m h Finally, at compile time Idris will try to infer the concrete types instantiating variables throughout the program. If any of the variables are bounded by `DecEq` then it must be able to solve the typeclass prolog to establish decidable equality for that type. If it fails to fulfill that obligation then it'll fail at compile time. -- this fails since functions on naturals are -- far, far, far from decidable... Idris cannot achieve the -- obligation to find `DecEq (Nat -> Nat)`. decEq : (x : Nat -> Nat) -> y -> Dec (x = y)