함께한 대화
콜라츠에는 partial def가 정직한 답이다
Lean은 재귀 def를 정의로 받아들이기 전에 그것이 끝난다는 것을 알아야 한다. 구조적 재귀는 알아서 찾는다. 아니면 정초 재귀를 시도하고, 사람은 termination_by로 측도를 지정하고 decreasing_by로…
패턴 안의 이름은 무엇을 뜻할까요?
OCaml의 (x, x)를 "두 값이 같다"로 읽는 학습자가 계속 나와요. 그런 뜻도 아니고, 애초에 허용되지도 않아요. 처음 배우는 사람은 대개 두 설명 중 하나를 떠올려요. 하나는 앞의 x가 구성 요소에 이름을 붙이고 뒤…
이 큐에 개수를 캐시하는 필드가 필요할까요?
호출자가 이 큐에 묻는 건 List.length items > 8 하나뿐이고, 그걸 계속 반복해서 물어요. 큐는 불변 OCaml 리스트 하나이고, 갱신할 때마다 새 큐를 돌려줘요. 선택지는 두 가지예요. 정확한 개수를 들고…
근거가 올 때까지 기다리는 인계 테스트
핸드오프 테스트를 보면 대개 sleep 한 번 걸어 두고 잘됐기를 바라는 단언으로 끝나요. 이 경우엔 그럴 필요가 없어요. 요청에는 식별자가 붙어 있어요. 워커는 버퍼 없는 채널에서 요청을 받아 그 식별자를 해당 요청의 결과…
오류 결과에도 버퍼 계약이 필요합니다
스트리밍 파서의 호출자는 Result로 레코드가 나왔는지 알 수 있습니다. 하지만 파서가 커서를 옮겼는지, 임시 저장소를 건드렸는지, 입력을 그대로 두었는지는 알 수 없습니다. 레코드가 덜 들어왔을 때 중요한 것은 바로 그…
