# Standard ML到底应该使用哪个工具链？

MLton？SML/NJ？PolyML？

# fcom就是hcom的一种特殊形式吗？

Fcom = formal composition

http://www.cs.cmu.edu/~rwh/talks/POPL18-Tutorial.pdf

# What should we return when pattern matching on a Higher Indutive Type and the case is a Path?

Context: Cubical Type Theory

Consider a simple HIT, say, an HitInt:

data HitInt : Set where
pos : (n : ℕ) → HitInt
neg : (n : ℕ) → HitInt
posneg : pos 0 ≡ neg 0



Or, if you don't speak Agda we can use cubicaltt:

data int = pos (n : nat)
| neg (n : nat)
| zeroP <i> [ (i = 0) -> pos zero
, (i = 1) -> neg zero ]



We want to define, for instance, a succ operation for it. As a functional programmer, we want to pattern matching on this HIT. In Agda, it's:

sucHitInt : HitInt → HitInt
sucHitInt (pos n) = pos (suc n)
sucHitInt (neg zero) = pos 1
sucHitInt (neg (suc n)) = neg n
sucHitInt (posneg x) = pos 1



Or in cubicaltt:

sucInt : int -> int = split
pos n -> pos (suc n)
neg n -> sucNat n
where sucNat : nat -> int = split
zero -> pos one
suc n -> neg n
zeroP @ i -> pos one



What I'm interested in is the last case-split of these two pattern matchings. The function is supposed to return the successor of the input integer, but we need to implement something that "finds the successor of the input _Path_".

My question is, how are we supposed to implement this case-split? In the cubicaltt version (taken from the cubicaltt's GitHub repository, examples/integer.ctt), it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer. Is this really what we want to do? Why it's not returning a Path like <i> pos 1 (even this is not a member of the higher inductive family)?

What's interesting is that, in Agda it'll fill pos 1 in the case body when I use Agda's proof-search.

# What does "Kan" mean in "Kan operations"?

I'm studying Cubical Type Theory and I see the word "Kan operations" (ref1, ref2, ref3, and there are many more), which is related to "adding a cap to a tube" (can be also explained as "given a path between a and b, and two paths that are between a and c/b and d respectively, we can use Kan operations to get a path between c and d").

I wonder if there's any references that can explain where this "Kan" word come from -- what does it mean? Is that "Kan extensions" in Category theory?

# 如何评价YACC Type Theory？

YACC是Yet Another Cartesian Cubical，不是那个Parser Generator