coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] PHOAS with extrinsic typing?
Date: Tue, 26 Nov 2019 16:58:47 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f50.google.com
Ironport-phdr: 9a23:CJeM/BJf8tnlZEr+R9mcpTZWNBhigK39O0sv0rFitYgRI/XxwZ3uMQTl6Ol3ixeRBMOHsqkC0rSN+Pm9ByQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngi6oATfu8UZnIdvKqc8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9Drx2hqR5wzY7abo+WKfRwYL/ScMgASmZdRMtcTTBNDp++YoYJEuEPPfxYr474p1YWqRWxHxKsBOTpyjRVh3H2x6o60/86EQrb2wEgHcgBsG/TrNXzO6cSS+e1zLLTzTjHdP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjLgFKQqYn/MDOU0OQAq3Ob7/Z6Wu2ziG4otQ5wrSSvxsg2jInJiZwaxkrY+iV+xYY5PcG3SE5/Yd6lCJtfrSWaOJFsTsMkXW5opCA3waAFt56jZCUG1ogryhrFZ/GEc4WE+AzvWPqSLDtihH9pZLSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx51mu1iuS2wzK5OFJIVw4mbDUK54mxb4wmZ4TvlrZEiDqn0X2ibeadkQi+ue29+TqeqvqqoOYOoNuiQzzMr4iltKjDek7KAQDX3SX9fy51LL5/E35RLtKjucxkqncqJ3aJ94UprW+Aw9T3YYj8RG/Dyy90NkchnQHI1dFdwiGj4jtIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaCaiAdajWrFXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKIugxpwRIF+iGe99axGbaGHrhNgbFnwR7yIxSeXrjBuJVjsFNCX6ZL41+jxuUNHuNozEXI342OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMXCdJ8ZglnoPUr3zEtZ9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/B54w1aHlKV02rlWSIQV6PROXQM3c5Xbyr4iBg==

I've posted an answer at https://cstheory.stackexchange.com/a/45929/32165

On Tue, Nov 26, 2019 at 4:23 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

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