UlfNorell
commented
10 years ago From nils.anders.danielsson on May 28, 2013 07:36:44
Hence, it seems to me that Agda could be enhanced to accept logical relations even when encoded as datatypes without compromising consistency.
Perhaps, but this is not entirely obvious to me.
This issue seems related to issue 840 , where Andreas states that "This is another instance where positivity and termination checker would need to cooperate". (I'm not quite sure what other instances he had in mind.)
Labels: Type-Enhancement
From p.giarrusso on May 27, 2013 22:40:12
Strict positivity checking prevents encoding logical relations as datatypes. However, an equivalent datatype can be encoded using a recursive function, because Agda's termination checker can prove the function is terminating, as shown below. However, needing to use a different encoding creates at least an unnecessary syntactic difference, and requires using a universe of types.
Hence, it seems to me that Agda could be enhanced to accept logical relations even when encoded as datatypes without compromising consistency. In general, it seems Agda could accept not strictly positive recursion in a datatype as long as the recursion is terminating. (Or I'm missing some deep reason why this is
module BugLR where
open import Data.Bool
-- A minimal universe for STLC: data Type : Set where ⇒ : (τ₁ τ₂ : Type) → Type bool : Type
infixr 5 ⇒
⟦_⟧ : Type -> Set ⟦ τ₁ ⇒ τ₂ ⟧ = ⟦ τ₁ ⟧ → ⟦ τ₂ ⟧ ⟦ bool ⟧ = Bool
data Condition : {T : Type} → ⟦ T ⟧ → ⟦ T ⟧ → Set where foo : ∀ {T} (v : ⟦ T ⟧) → Condition v v
-- Not actually a logical relation! Also note this could be encoded without using a universe as a datatype in Set 1. data ValidityLogicalRelation : {T : Type} → ⟦ T ⟧ → ⟦ T ⟧ → Set where base : (v1 v2 : Bool) → Condition v1 v2 → ValidityLogicalRelation {bool} v1 v2 fun : ∀ {S T} → (v1 v2 : ⟦ S ⇒ T ⟧) → -- The extra argument gives a positivity error: ((s1 s2 : ⟦ S ⟧) → {- ValidityLogicalRelation s1 s2 → -} ValidityLogicalRelation (v1 s1) (v2 s2)) → ValidityLogicalRelation v1 v2
-- This is actually a logical relation. ValidityLogicalRelation2 : {T : Type} → ⟦ T ⟧ → ⟦ T ⟧ → Set ValidityLogicalRelation2 {bool} v1 v2 = Condition v1 v2 ValidityLogicalRelation2 {S ⇒ T} f1 f2 = ((s1 s2 : ⟦ S ⟧) → ValidityLogicalRelation2 s1 s2 → ValidityLogicalRelation (f1 s1) (f2 s2))
Now, we know that non-strictly-positive datatypes are bad and cause non-termination. Does the above encoding show a weakness in Agda? Not at all, because datatypes we can encode are all non-problematic.
If we try to apply the same encoding to the example from the wiki ( http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.SimpleInductiveTypes?from=ReferenceManual.Datatypes#Strictpositivity ), we get a non-terminating recursive definition:
{- data Bad : Set where bad : (Bad -> Bad) -> Bad -- A B C -- A is in a negative position, B and C are OK -} -- The above datatype is encoded by: Bad : Set Bad = (Bad → Bad)
but the above function definition can readily be rejected by Agda's termination checker.
I think the above encoding still wouldn't allow embedding HOAS terms, because their definition is not type-directed and the recursion is not decreasing on the size of the type. So maybe such an extension (if possible at all) would not be so extremely useful, but that's not for me to decide.
Original issue: http://code.google.com/p/agda/issues/detail?id=861