iOSDC Japan 2019에서 "Swift와 논리+코일론"발표

안녕하십니까?
올해도 관례대로 iOS의 썸머 페스티벌 행사@inamiy(2019년 9월 5~7일)에 참여해 아이윌블로그를 진행했다.
올해로 4년째인 만큼 개최 기간이 3.5→2.5일로 단축되고 60분의 긴 등단 인원이 추가돼 지난해보다 CfP 당선자 수가 줄어들 것으로 예상돼 격전이 예상된다.
이번에는 오래전부터'스위프트와 논리(칼리 호워드 대응)'를 주제로 이야기하기로 했지만 충격적인 제목에서 탈락을 판단하고 부제를 붙여 서둘러 말을 담았다.
iOSDC Japan 2019, 종합적인 내용(억지로) 확장과 동시에 붐비게 될'정규 연설틀'을 회피하고'기술 예수 수난기 공유연설'로 응모하는 등 필사적으로 고려할 수 있는 최선의 선택을 얻었다.
결과가 순조롭게 당선되어 기뻤지만 제목이 너무 커서 전날 슬라이드 제작까지 고전하며 참회했습니다.

당일 발표 내용

이날 발표는 다음과 같다.

가짜 원숭이: 작년의'권론'이야기

슬라이드: Swift 프로그래밍과 논리~ 그리고 돌아온 코일론~ by 벼견태홍｜담화｜iOSDC Japan 2019 #iosdc-fortee.jp

비디오: (TBD)

샘플 코드: https://speakerdeck.com/inamiy/swift-and-logic-and-category-theory

그 중에서 몇 가지 개인적인 하이라이트를 들면 가장 간단하고 미친 실현은 다음과 같은'모순율'absurd 함수다.

/// `⊥ ===> A`
func absurd<A>(_ x: Never) -> A {
    // Swift 5.1 では何も書かなくて良い ¯\_(ツ)_/¯
}

Swift5.1은 역할 영역에 아무것도 설치되어 있지 않아도 컴파일할 수 있습니다.
이것에 상당히 놀란 사람도 많지 않습니까?
(Swift5.0 이하일 경우switch x {} 설치 빈 모드와 일치하면 됨)
또한 고전 논리와 https://github.com/inamiy/SwiftAndLogic의 차이에 대한 간단한 설명으로서'볼의 두 가지 선택은 닫힌 세계'와'무한 확장형 세계'의 해석이 다르다는 것을 알 수 있다.
Bool의 세계에서 부정true은 false(=true 이외의 값)이지만 유형의 세계에서 부정Int은'Int 이외의 (무한존재) 유형'(무한존재가 없기 때문에)으로 해석할 수 없고 Int -> Never으로 표시되는 함수 유형이다.
(수학적으로 볼 대수의'보원'은 성립되지 않고 고급 대수로 해석된다직관주의 이론
그리고 우리는 그린정리(Glivenko's theorem)라고 불리는 이중 부정의 번역을 더해 고전 논리를 직관주의 논리(≈Swift의 세계)로 유인하는 것을 보았다.
예를 들어 배중률이라면'아무것도 없는 곳(빈 파라미터)에서 제작Either<A, Not<A>>'과 같은 억지 게임을'Not<Either<A, Not<A>>>에서 제작Never'과 같은 설치형 수수께끼로 전환한다.
자세한 내용은 위 슬라이드와 샘플 코드를 참조하시고 Swift Playground 등을 꼭 즐기시기 바랍니다.
그나저나 이날은 권론에 대해 설명할 수는 없지만 권론의 도식을 사용하면 언뜻 보면 비대칭 논리학의 AND와 OR의 추리 규칙은 권론의 쌍대성 대칭에 따라 설명할 수 있는 것 외에 수반, 멱 대상, 피리칼 폐권과 논리의 관계, 토폴로지 사용의 의미론 등 화제와 연결된다.
이렇게 논리를 바탕으로 권론, 논리와 프로그래밍, 권론을 배우는 시도가 완성되었다.
Swift뿐만 아니라 금형을 배우는 프로그래머들의 참고가 될 수 있다면 좋겠다.

마지막

이처럼 매일 iOS 개발 현장에서 1구경도 소용이 없으면 발표할 수 있고 교류할 수 있다는 것이 iOSDC의 매력이다.
올해 드디어 참가자가 1000명을 넘어섰으니 내년 개최가 갈수록 기대된다.
스태프 여러분, 스피커·참가자 여러분, 올해도 수고하셨습니다 & 감사합니다!
내년까지 받은 전자 블록으로 홈팟을 만들고 싶어요!!
스태프들의 추천으로 학연 전자 블록을 받게 될 줄은 몰랐어요!정말 감사합니다.내년에는 이걸 Swift와 연계해서 열심히 발표하도록 하겠습니다.💪 "의보원" #iosdc — Yasuhiro Inami (@inamiy) pic.twitter.com/cv4IMfXASf