Is there a general way to derive these computation rules?

[ice1000]

I saw

yacctt/Eval.hs

Lines 428 to 433 in 72cf547

	Ter (Sum _ n nass) env
	| n `elem` ["nat","Z","bool"] -> return u -- hardcode hack
	| otherwise -> error $ "coe sum: " ++ show n
	Ter (HSum _ n nass) env
	| n `elem` ["S1","S2","S3"] -> return u -- hardcode hack
	| otherwise -> error "coe hsum"

Is it that you are too lazy to implement the general case, or is it an open problem?

[mortberg]

We were just too lazy. One can introduce a special universe of types where coe computes like the identity function. I think one of the RedPRL/redtt/cooltt implementations did this, but I don't remember which or how it worked in detail... @favonia @jonsterling @cangiuli

[mortberg]

Btw, with this hack it's obviously easy to do bad things. Just have a type with parameters called "S1" and make some coercion that shouldn't compute like the identity. However, as we don't have a termination checker it's already trivial to prove false so we didn't consider this too bad. Plus the only intended users of yacctt were the developers who knew about all of the hacks :-)

[ice1000]

Nice, thanks! In what case would hcom on HIT compute like an id function? My current understanding is that hcom on HIT is mostly canonical and sometimes reducible as id, am I right?

[ice1000]

A friend told me it's when your type is not parameterized, but I actually don't quite understand why it works this way. I guess I'll need to read some papers.

[mortberg]

A friend told me it's when your type is not parameterized, but I actually don't quite understand why it works this way. I guess I'll need to read some papers.

Are you talking about hcom or coe? For coe this is correct, for hcom it's not. My recommendation is not to just read some papers, but to try to check this yourself on paper. (Hint: think about a universe U.)

[ice1000]

Thanks for the clarification, I think my friend told me about coe, and I was asking about hcom.