All Questions
29
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 ...
0
votes
2
answers
138
views
Default Implementation of Coq typeclass methods
Is there a way you can provide default implementations of Coq typeclass methods like you can in Haskell? I saw no mention of this in the Coq typeclass documentation. If there does not exist such a ...
- 5
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
2
answers
188
views
Coq: Strong specification of haskell's Replicate function
I'm having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it ...
- 99
1
vote
1
answer
405
views
How to constrain a type field to a power of two in a type system? [duplicate]
There is this in some JavaScript code:
function allocate(bits) {
if ((bits & (bits - 1)) != 0) {
throw "Parameter is not a power of 2";
}
...
}
Essentially, there is a ...
- 77.9k
1
vote
1
answer
310
views
Coq extraction to Haskell
I have the following Coq implementation of integer division with remainder.
When I extract it to Haskell everything works fine. I compared the Coq version to the generated Haskell version and tried to ...
- 6,760
7
votes
2
answers
357
views
Proofs' role in Coq extractions
I'm trying to understand what is the role of proofs in Coq extractions.
I have the following example of floor integer division by two taken from here. For my first try I used the Admitted keyword:
(**...
- 6,760
1
vote
1
answer
281
views
Extracting Prop from Coq to Haskell results in empty type
I'm trying to make sure that a useless Prop is discarded when extracting Coq to Haskell. However, when I use the following example, I see that both divides and prime are extracted as Haskell empty ...
- 6,760
0
votes
1
answer
152
views
Predict running times of extracted Coq code to Haskell
I have the following version of isPrime written (and proved) in Coq.
It takes around 30 seconds for Compute (isPrime 330)
to finish on my machine.
The extracted Haskell code takes around 1 second to ...
- 6,760
6
votes
1
answer
173
views
Extracting Coq to Haskell while keeping comments
Is there anyway to keep comments while extracting Coq to Haskell?
Ideally, I would like to have machine generated Haskell files untouched by humans, and so the motivation of extracting comments is ...
- 6,760
7
votes
2
answers
2k
views
Extracting Coq to Haskell
I'm experimenting with Coq's extraction mechanism to Haskell. I wrote a naive predicate for prime numbers in Coq, here it is:
(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith....
- 6,760
4
votes
1
answer
299
views
Church encoding for dependent types: from Coq to Haskell
In Coq I can define a Church encoding for lists of length n:
Definition listn (A : Type) : nat -> Type :=
fun m => forall (X : nat -> Type), X 0 -> (forall m, A -> X m -> X (S m)) -&...
- 1,733
8
votes
0
answers
470
views
Is it possible to normalize affine λ-calculus terms using PHOAS in Agda?
In Agda, one can conveniently represent λ-terms using PHOAS:
data Term (V : Set) : Set where
var : V → Term V
abs : (V → Term V) → Term V
app : Term V → Term V → Term V
That approach has ...
- 52.4k
1
vote
2
answers
175
views
Representing Functions as Types
A function can be a highly nested structure:
function a(x) {
return b(c(x), d(e(f(x), g())))
}
First, wondering if a function has an instance. That is, the evaluation of the function being the ...
- 77.9k
9
votes
1
answer
236
views
Can you automatically add Haskell import statements when extracting from Coq?
I'm doing an extraction from Coq to Haskell that requires importing a couple of modules on the Haskell end. Is there any Coq extraction feature that allows you to do this automatically? I know I ...
- 423