coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] PHOAS with extrinsic typing?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] PHOAS with extrinsic typing?
Date: Tue, 26 Nov 2019 16:22:31 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:Osr+5R+ISvkxXf9uRHKM819IXTAuvvDOBiVQ1KB42+4cTK2v8tzYMVDF4r011RmVBN6dsqwfwLOK4+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVijexe65+IRS4oAneq8UbjohvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFokaxVvhyhqRx8zYDabo6aO/hxcb/GcNwAWWZMRNxcWzBPD46+aYYEEuoPPfxfr4n4v1YDsQaxChOpBOjy1DJIhnv23awi0+s7FQHJxhErEtUUv3vJttr1MbsdXPupw6nT1zrDbvdW1S346IjJbhAtu++DUq9tccfIz0QkCg3LjlKVqYP/PjOV0PwAvHSb7+pkVOKvk3QoqwVrrTS1wMcjlJXJi4QIwV7H7SV02Js5KcO7RUJhb9OoDIFcuz+AO4doX88uX3lktDskxrAFo5K2cjQGxI4jyhLBcfCLbZaE7g/lWe2MOzl3nmhld6i6hxuq8Uiv1On8Vs6s3VZNsypFjtbMtncM1xzV5ciLU+B9/lu71jaTzQ/f8P1LIVsumqraL54t2LswlpsPsUjZACD5hVj2gLeXdkUi5Oeo9/zqbqj4qpKfLYN5hB3yPr4wlsClH+g0LxQCU3Ce+eum1b3j+UP5QK9Njv0ziqTWqo3VKt4epqGlGAJazp0j5Ay+DzeiytgYmHgHLE5fdB2ZkofpJknCIOrkAvenn1SsjDBryujaMb3mG5XBN2TMkLP8fblm8ENc0woyzdVH551OEL0BIfTzWlXwtNPCFBM5PRa0kK7bD4B20ZpbUmaSCIeYNrnTuBmG/LEBOe6JMaYZsTO1APgh5ubniXZxzVYRdKyi9ZAMYXG8WPFnPwOUbWe60YRJKnsDogdrFL+is1aFSzMGPy/vDZJ53SkyDcedNamGRo2ph+fZjiCmApJRZ2ZJT0uQGGvhMY6fUvYILieTPolsniFWDeH9Gb9k7gmnsUrB85QiNvDdo3BKvonq1dwz4uzP0xw+6G4sVpXP4yS2V2hx21gwaXoz1aF7r1Z6zw7eg6Njiv1cU9lS+7VEXhpobJM=

Here's a coarse first response: PHOAS works pretty well to encode syntax & semantics of untyped languages, and perhaps there is a similarly smooth way to add a typing relation on top (I've never tried personally).

On 11/26/19 3:41 PM, Joey Eremondi wrote:

The problem I have is that, I would like to use PHOAS to model a dependently typed calculus. Having terms and types be in the same syntactic category means that (as far as I can see) the extrinsic approach is not feasible: we can't have `term (V : Set) : term -> Set `.

[Coq-Club] PHOAS with extrinsic typing?, Joey Eremondi, 11/26/2019
- Re: [Coq-Club] PHOAS with extrinsic typing?, Adam Chlipala, 11/26/2019
  - Re: [Coq-Club] PHOAS with extrinsic typing?, Jason Gross, 11/26/2019