All Questions
48
questions
-4
votes
1
answer
335
views
Can a dependently typed language be Turing complete? [closed]
It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of ...
2
votes
1
answer
338
views
Agda: Failed to solve the following constraints: P x <= _X_53 (blocked on _X_53)
I'm writing Agda code as I read the HoTT book. I'm stuck on Lemma 2.3.9:
data _≡_ {X : Set} : X -> X -> Set where
refl : {x : X} -> x ≡ x
infix 4 _≡_
-- Lemma 2.1.2
_·_ : {A : Set} {x y z ...
2
votes
1
answer
165
views
Can I prove "coinductive principles" about coinductive type?
Can I prove "coinductive principles" about coinductive type? For example, the pseudo code of the coinductive principle for the stream type would look like this:
Π P : Stream A -> Type.
Π ...
- 410
2
votes
4
answers
391
views
Is flattening a list easier in dependently typed functional programming languages?
While looking for a function in haskell that flattens arbitrarily deeply nested lists, i.e. a function that applies concat recursively and stops at the last iteration (with a non-nested list), I noted ...
- 453
4
votes
1
answer
280
views
Can I safely assume that isomorphic types are equal?
Let A and B be Types, and f : A -> B and g : B -> A be functions inverse to each other. In other words A and B are isomorphic types.
Is it true that one cannot prove that A <> B?
Can I ...
- 1,733
14
votes
3
answers
2k
views
Why do Calculus of Construction based languages use Setoids so much?
One finds that Setoids are widely used in languages such as Agda, Coq, ... Indeed languages such as Lean have argued that they could help avoid "Setoid Hell". What is the reason for using ...
- 2,136
2
votes
1
answer
157
views
Agda equivalent of `destruct <term> eqn:<identifier>` [duplicate]
I understand that Agda does case analysis using with-clauses, which is similar Coq's destruct tactic. The destruct tactic has a variant of the form destruct <term> eqn:<identifier>, which ...
- 150
3
votes
2
answers
325
views
How do define a custom induction principle in coq?
This is kind of a follow up on a previous question I asked, but now I'm just trying to implement my own induction principle for the equality type, which I'm not sure how to do without some kind of ...
user5775230
2
votes
1
answer
244
views
How to explicitly use an induction principle in coq?
I'm trying to prove symmetry of propositional identity with the induction principal explicitly in Coq, but can't do it with the induction principle like I can in agda. I don't know how to locally ...
user5775230
1
vote
1
answer
244
views
Translating Coq Definitions to agda?
I'm wondering if there is a systematic way to interpret Coq Definitions as agda programs. I'm working through translating part of programming foundations and am not able to get the tUpdate function ...
user5775230
5
votes
2
answers
482
views
How does one use the with inspect in Agda?
I'm trying to reproduce a very simple coq proof from Programming foundations in agda, and was told I need to use the with inspect to prove a contradction from the pattern match on the (bool) ...
user5775230
80
votes
1
answer
2k
views
Why is my definition not allowed because of strict positivity?
I have the following two definitions that result in two different error messages.
The first definition is declined because of strict positivity and the second one because of a universe inconsistency.
(...
- 1,480
1
vote
2
answers
646
views
Church encoding of dependent pair
One can easily Church-encode pairs like that:
Definition prod (X Y:Set) : Set := forall (Z : Set), (X -> Y -> Z) -> Z.
Definition pair (X Y:Set)(x:X)(y:Y) : prod X Y := fun Z xy => xy x ...
- 1,733
1
vote
1
answer
172
views
Induction principle for `le`
For the inductive type nat, the generated induction principle uses the constructors O and S in its statement:
Inductive nat : Set := O : nat | S : nat -> nat
nat_ind
: forall P : nat -> Prop,...
- 1,733
6
votes
1
answer
616
views
Why we cannot pattern match on Set/Type in Coq/Agda/Idris？
Think about a function which accepts a Set, and returns its byte length, named byteLength:
byteLength : Set -> Maybe Nat
and if I want to implement this function directly, I need to pattern match ...
- 3,775