coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Huet's Zipper

From: "Harrison, William L." <harrisonwl AT missouri.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Huet's Zipper
Date: Sat, 13 Jan 2018 17:53:09 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=harrisonwl AT missouri.edu; spf=Pass smtp.mailfrom=harrisonwl AT missouri.edu; spf=None smtp.helo=postmaster AT um-kip5-missouri-out.um.umsystem.edu
Ironport-phdr: 9a23:anrJeBbkEAWHWwySi45CNxX/LSx+4OfEezUN459isYplN5qZr8m+bnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhymphxw34HbbZqPO/Zie6PQZ9MaSXZDU8tXSidPApm8b4wKD+cZM+pWrZPyp0EUrRu/HgmsA+XvxidVjXD23K061+AhEQDc0wwlAtkAtm7YoNvoP6oVUeC61rPIzS/Cb/NN3jf97obJchQ6rPGJXLJwatHRyU4yFwPfj1Wcs5LqMC6I1ukUtWWQ8uluVfq3hmI5tw18piKjytowhoTInI4Z1E7I+CFjzIorONG0VlZ3bcOmHZZerS2XOZZ6Ttk8T210pio20KMKtJC7cSQS1Zgqwx3SZ+aZf4SU5h/vTuacLDZiiH54ZL6ygQu5/1K6xe3mTMa01U5HripbndnIsXAAzwHT6s2eRvt+/0ehwTaC2xnW6uFFOkA0jq3bK4M7wr4xj5YTtlnDHjPslEXria+abFgk+u2z6+XnebXmuoGTN4puhg7gL6suh9SzAeU+MgcQQ2iW4fqw2KHn8EHjXblGkvw7nrPHvJzEIckXvLC1DxJL3oo77hawFTam0NAWnXkdK1JFfQqKj4jzNFHUOvD4DOy/g1OqkDZlw/DLJbjhApTWLnjYl7fhYKx9609GxAUt0N9f+opYCqsdL/LrRk/xqNvYAwclPAyz2ubrEcly1ocDWW2UGaKZK6PTsVqQ5u01OeWMZYkVuCz8K/c//fLug2U5yhchevzj1pwOLXu8A/5OIkODYHOqjM1LWTMBuRN7R+j3gnWDVyRSbjC8RfRvyCs8DdfsLY7ZXIG2h7rFlBi6GplXb2UOLhbGWSPofp+eWuwLbj2WCspgiScDSKKgDYItyEf950fB17N7I7+MqWUjvpX52Y0tvryBpVQJ7TVxSv+l/SSIRmBwkHkPQmZqjqV+uld6102Cl6V0nq4BTIAB17ZySg4/cKXk4aliEdmrBlDEf8yST0u8Q5OrDSxjFotske9LWF50HpCZtj6G3yeuBORFxaGOQZ816v+Z2nnqPMFg0XeD07Q9yUQjBNZKLny9mqN6sQXfGtyRng==

I’m wondering if what Vene and Uustalu call “causal tree comonads” (in "Comonadic functional attribute evaluation”, TFP05) has ever been developed in Coq? A well-known example of such comonads is Huet’s “zipper” (from “The Zipper”, JFP97). Here is some Haskell code from Uustalu & Vene that defines the associated functor (CxtTree e):

data Tree e a = a :< Trunk e (Tree e a)

data Trunk e a = Leaf e | Bin a a

-- CxtTree is Huet's "zipper"; i.e., a tree with a path into it.

data CxtTree e a = Cxt e a :=| Tree e a

data Cxt e a = Empty | Cxt e a :> Either (a,Tree e a) (a,Tree e a) deriving Show

I’m particularly interested in a development in Coq in which (Tree e)is (potentially) infinite.

Thanks in advance,

Bill

[Coq-Club] Huet's Zipper, Harrison, William L., 01/13/2018