winterkoninkje | Entries tagged with coq

This is a followup to a recent post on Parameterized Monads which I discovered independently, along with everyone else :)

For anyone interested in reading more about them, Oleg Kiselyov also discovered them independently, and developed some Haskell supporting code. Coq supporting code by Matthieu Sozeau is also available. And apparently Robert Atkey investigated them thoroughly in 2006.

If people are interested in more Coq support, I've been working on a Coq library for basic monadic coding in a desperate attempt to make programming (rather than theorem proving) viable in Coq. Eventually I'll post a link to the library which will include parameterized monads as well as traditional monads, applicative functors, and other basic category theoretic goodies. This library along with the Vecs library I never announced stemmed from work last term on proving compiler correctness for a dependently typed language. Hopefully there'll be more news about that this fall.

I've a question for any Coq users out there. How can you provide type equality constraints when doing case matching (ala GADT case matching in Haskell)? That is, assume we've defined something like:

Inductive Stack {A:Set} : nat -> nat -> Set :=
    | stack : (m:nat) -> (n:nat) -> vector A m -> vector A n -> Stack m n.

And now we want to do something like:

Definition
    foo {A:Set} {m n : nat} (s : stack (S m) n) (f : stack m (S n) -> (stack m (S n) *...)) ...
    := ...
        match s with
        | (stack (S m0) n0 (Vcons x0 _m0 xs0) ys0) =>
            let s' := stack m0 (S n0) xs0 (Vcons _ x0 n0 ys0)
            in match f s' with
               | (stack m1 (S n1) xs1 (Vcons y1 _n1 ys1), ...
               end
        end.

Where the type of f is constrained to accept and return stacks with the "right" indices with respect to the parameter s. I keep running into this problem where information about the length indices (i.e., what they're unified with) is getting lost by either one case match or the other. Hopefully I haven't simplified the example so much that you can't see why that would come up. I've tried playing around with different forms of match and moving around the arguments to Stack/stack to no avail. And my google-fu is failing me. Halp!

( Edit: solution, for posterity )

S	M	T	W	T	F	S
	1	2	3	4	5	6
7	8	9	10	11	12	13
14	15	16	17	18	19	20
21	22	23	24	25	26	27
28	29	30

Renaissance Grrrl

Entries tagged with coq

Generalizing Monads (redux)

LazyWeb to the rescue?

Profile

April 2019

Posts

Where next?