Super Haskell: an introduction to Agda by André Muricy.mdx

[https://www.youtube.com/watch?v=OSDgVxdP20g

예, 라이브 방송입니다. 안녕하세요 여러분, 따뜻하게 FunR에 오신 것을 환영합니다.

이번에는 스웨덴입니다. 올해 두 번째 방문이네요. 우리는 지금 스톡홀름에 있는 KRA 사무실에 있습니다. 정말 멋진 사무실이네요. 저희를 이 멋진 스톡홀름 사무실에 초대해 주셔서 KRA에 진심으로 감사드립니다.

정말 감사합니다. 바로 시작하겠습니다. 먼저 저 Magnus가 짧게 소개를 하고, 그다음 Andrea가 Super Husc, Agda 소개를 할 것입니다. 그 후에는 Lash가 Scala를 이용한 스키마 관리에 대해 발표할 것입니다.

재밌는 사실은 Lash는 원래 3년 반 전에 이 발표를 하기로 되어 있었는데 코로나가 발생하면서 3년 반이 지난 지금, 드디어 여기서 발표를 하게 되었습니다. 정말 기쁩니다.

네, 정말 기쁩니다. 마지막에는 제가 다시 한번 Meetup을 요약할 것입니다. 저희를 이곳에 초대해 주셔서 KRA에 다시 한번 감사드립니다. KRA 직원들과 이야기하고 싶으시면 초록색 옷을 입은 사람들을 찾으세요.

초록색, 네. 또한 비디오 스트림을 후원해 주신 Other The Beat에도 감사드립니다. Other The Beat에 대해 더 알고 싶으시면 인터넷을 참고하세요.

그리고 올해 남은 일정은 11월 7일에 또 다른 Meetup으로 돌아오고 12월 5일에도 Meetup이 있습니다. 1월에는 아직 날짜를 정하지 않았지만 물론 Meetup이 있을 것입니다.

FunR Sweden Meetup을 지원하고 싶으시면 Meetup으로 이동하여 Meetup 커뮤니티에 가입하세요. 매우 간단합니다.

그리고 물론 YouTube로 이동하여 구독, 좋아요 등 YouTube에서 할 수 있는 모든 것을 하세요. Google이 여러분을 좋아할 것이고, 저희도 여러분을 좋아할 것입니다.

그리고 저희는 Discord 채널도 개설했습니다. YouTube 채팅에서 긴 질문을 하기 어려울 때가 있습니다. Discord에 참여하시면 발표자에게 길고 까다로운 질문을 할 수 있습니다.

그래서 발표 중에 질문이 있으시면 채팅이나 Discord 채널에 올려주시거나, 여기에 계시다면 손을 들어주세요. 질문이 있으신가요?

네, 그럼 시작하겠습니다. 첫 번째 발표는 Andrea의 Super Husc, Agda 소개입니다.

환영합니다, Andrea. 노트북을 넘겨드리겠습니다. 감사합니다, Magnus.

네, 감사합니다.

좋아요, 마이크가 작동하는군요. 여기서 확인해 보죠.

시작하겠습니다. 참석해 주시고 제 강연을 들어주셔서 감사합니다. 잠시 제 폰으로 설정을 좀 하겠습니다.

이제 시작해 볼까요? 제가 Super Haskell이라고 부르는 언어를 탐험해 보겠습니다.

먼저 저를 간단히 소개하겠습니다. 저는 브라질 출신의 소프트웨어 엔지니어이지만 스웨덴에 약 3년 동안 살고 있습니다. Adatabt에서 FP 컨설턴트로 일하고 있으며, 요즘에는 Purescript를 사용하고 있습니다. 예테보리 대학교에서 석사 학위를 받았고, 범주론과 동적 시스템을 Agda로 연구했습니다. 물론 저는 Agda 전문가는 아닙니다.

그 점을 미리 말씀드리고 싶지만, 여러분의 흥미를 끌 만큼은 충분히 알고 있다고 생각합니다. 이 강연은 제 생각에는 아주 대략적인 추정이지만 TI가 많은 부분을 차지할 것 같습니다. Agda 언어와 그 기반 이론에 대한 철학과 동기 부여를 조금 다루고, Agda의 핵심 개념을 소개하는 코드 예제를 살펴본 후 Agda를 사용하여 매우 작지만 실제적인 프로그램을 실행해 보겠습니다.

**우선 왜 디팬던트 타입을 사용해야 할까요? 왜 디팬던트 타입을 사용하는 프로그래밍을 해야 할까요? 제가 생각하기에 코드를 작성할 때, 소프트웨어 엔지니어링을 할 때, 우리는 일반적으로 코드가 정확한지 여부에 신경 씁니다. 저는 이것을 두 가지 유형의 작업으로 봅니다. 하나는 코드를 구현하는 것입니다. 즉, 함수의 본문을 작성하는 것이죠. 하지만 또 다른 하나는 방금 작성한 코드에 대해 생각하고 정확성을 보장하며 실제로 원하는 대로 작동하는지 검증하는 것입니다. 이 그래프에서 '정확성 보장'과 '구현'이라는 용어는 매우 중복되어 있습니다. 프로그램을 정확하게 디버깅하는 데 필요한 신뢰도는 다양합니다. 즉, 상황에 따라 다른 기준을 가지게 되고 구현에 필요한 작업량도 달라집니다. 어떤 사람들은 Python으로 코드를 작성하는 것이 매우 쉽다고 생각할 것이고, 어떤 사람들은 Haskell이나 Agda, 또는 다른 언어로 코드를 작성하는 것이 쉽다고 생각할 것입니다. 저는 우리가 적절한 균형을 찾아야 한다고 생각합니다. 저는 조금 긴장되네요.

예를 들어, 소셜 미디어 웹사이트가 평소보다 느린 것보다 원자력 발전소 소프트웨어에 오류가 있는 것이 훨씬 더 심각합니다. 그리고 우리는 정확성을 보장하기 위해 몇 가지 도구를 사용할 수 있습니다. 테스트가 있지만, 분명히 완벽하지는 않습니다. 프로그램이 정확한지 확인하기 위해 가능한 모든 테스트를 생각해 낼 수는 없을 것입니다. 신뢰도 있습니다. 이것은 오랫동안 사용되어 왔고 오랫동안 잘 작동해 왔기 때문에 앞으로도 계속 작동할 가능성이 매우 높다는 것입니다. 이것은 린디 효과로 알려져 있습니다. 무언가가 영원히 존재해 왔다면 영원히 존재할 것입니다. 하지만 항상 그런 것은 아닙니다. 여기 계신 많은 분들이 Log4j 문제를 기억하실 것입니다. 아주 오래된 Java 라이브러리에 취약점이 있었는데, 제 생각에는 몇 년 전에 발견된 것 같습니다. 그리고 타입과 정리도 그것들이 실제로 말하는 대로 작동한다는 보장은 아닙니다. 즉, 신뢰도가 보장되지 않는다는 것입니다.

컴파일러에도 버그가 존재합니다. GHC 9.4.1에는 부동 소수점 오류가 있었고, 증명 검사기에는 불일치가 존재합니다. Agda의 확장 기능인 Cubical Agda의 개발 버전에서 불일치가 발견되었습니다. 이는 기본적으로 해당 버그를 악용하면 무엇이든 증명할 수 있다는 것을 의미합니다. 따라서 우리는 절대 확신할 수 없습니다.

물론 우리는 신뢰도를 높일 수 있습니다. Agda와 디팬던트 타입이 제공하려는 도구는 인간의 의도와 기계 코드 사이의 간극을 좁히는 것입니다. 즉, 전자가 전선에서 우리가 원하는 방식으로 움직이도록 하는 것입니다. '내가 의도한 바가 아니었어'라고 말하는 횟수를 줄이고 싶습니다. 그리고 이 맥락에서 타입에 대해 생각해 보면, 올바른 모양을 올바른 구멍에 넣어야 하는 어린이 장난감이 떠오릅니다. 제 생각에는 프로그래밍의 많은 부분이 이런 연결 작업으로 귀결됩니다. 여기서 비유하자면, 구멍의 모양은 함수를 호출할 때 넣어야 하는 것의 타입입니다. 그리고 구멍을 만드는 표면은 타입 시스템과 같습니다. 즉, 타입 시스템을 통해 특정 모양을 표현할 수 있습니다. 이제 올바른 모양을 올바른 구멍에 넣는다는 것이 무엇을 의미하는지 생각해 보겠습니다. 이 경우에는 H1 모양을 H1 구멍에 넣고 싶을 것입니다. 여기에 라벨을 붙이지는 않았지만 1, 2, 3이고 정사각형을 정사각형에, 원을 원에 넣고 싶을 것입니다. 이것을 보면 선택의 여지가 거의 없습니다. 물론 원을 정사각형 안에 넣을 수도 있지만, 그렇게 하려면 상당한 노력이 필요할 것입니다. 실제로는 모양을 가져다가 넣기만 하면 됩니다. 이것이 바로 이것이 전달하려는 내용입니다. 반면에 타입이 없는 언어에서는 모든 것이 정사각형과 같습니다. 이제는 정말 선택의 여지가 없습니다. 라벨을 읽고 '오른쪽에 있는 이것은 왼쪽 구멍에 들어가야 하는 것이고, 이것은 여기로 가고 저것은 저기로 가야 하는구나'라고 말해야 합니다. 즉, 더 많은 인지적 노력이 필요합니다. 제 생각에 Agda가 해당되는 Super Type 언어에서는 이러한 구멍의 모양을 매우 구체적으로 만들 수 있습니다. 즉, 타입 시스템을 통해 거의 모든 것을 표현할 수 있습니다. 그 안에 들어맞는 것은 단 하나뿐입니다.

하지만 비유를 계속 이어가자면, 이러한 구멍을 깎아내야 하는 표면에서 작업하고 있고 표면이 너무 약해서 작은 구멍을 만들거나 여기 조금 깎아내면 전체가 부서지고 저기에 작은 균열이 생길 수 있습니다. 이것은 우리가 원하는 것이 아닙니다. 반면에 너무 탄력적이면 이러한 구멍 중 하나를 가져다가 있는 힘껏 무언가를 밀어 넣으면 반대쪽으로 나오고 어떻게든 작동할 것입니다. 마치 TypeScript 코드에 any를 넣는 것과 같습니다. 따라서 우리는 적절한 재료를 원합니다. 제 생각에는 편의성과 정확성 사이에 적절한 균형점이 있습니다. 그리고 적절한 재료를 갖추지 못하는 경우는 두 가지 방향에서 발생할 수 있습니다. 하나는 타이핑 비용이 너무 높을 때입니다. 이 소식을 보셨는지 모르겠지만 최근에 Svelte가 TypeScript를 포기했습니다. 저는 그에 대해 잘 알지 못하지만, 실제로 이런 일이 일어날 것이라고는 예상하지 못했습니다. 지금까지는 일반적으로 모든 사람들이 모든 것에 타입을 계속 추가할 것이라고 생각했습니다. 왜냐하면 편의성의 비용이 높을 수 있기 때문입니다. 그래서 프로토타입을 만들기 쉽고 편리한 동적 타입 언어가 계속해서 타입 시스템을 추가하는 것입니다. 그리고 적절한 재료를 얻는 것은 어렵습니다. 이것은 제가 작업하고 있는 Purescript 라이브러리의 코드 조각입니다. 읽을 수 있는지 모르겠지만, 중요하지 않습니다. 요점은 이것이 코드의 벽이라는 것입니다. 그리고 이것은 그렇게 복잡하지 않은 것을 표현하고 있습니다.

그리고 여기에 타입에 대해 많이 알고 있는 정말 뛰어난 프로그래머인 Conor McBride의 답변이 있습니다. 그는 Haskell에 Singletons 라이브러리에 대해 말했습니다. 들어보셨는지 모르겠지만 기본적으로 Haskell에 디팬던트 타입을 모방하여 Haskell이 이미 가지고 있는 것보다 더 많은 타입 안전성을 추가하는 것입니다. 여기서 질문은 Singletons를 사용하면 무엇을 얻을 수 있는가였습니다. 그리고 그의 답변은 '그것은 우리가 다시는 보지 않기를 바라는 성가신 것입니다'였습니다. 하지만 저는 Agda가 이 균형을 맞추는 데 매우 근접했다고 생각합니다. 그리고 여기에 언어를 소개하는 슬라이드가 하나 더 있습니다.

Agda는 샬머스에서 개발된 디팬던트 타입의 순수 함수형 언어입니다. 문법은 Haskell과 매우 유사하지만 몇 가지 중요한 차이점이 있습니다. 곧 살펴보겠습니다. Hindley-Milner 대신 Martin-Löf 타입 이론을 기반으로 합니다. 왼쪽에 있는 분이 스웨덴 논리학자인 Martin-Löf입니다. 재밌는 사실은 Agda라는 이름이 Cornelis Vreeswijk의 노래에서 따왔다는 것입니다. 이것이 바로 그 아이콘입니다. 저는 이것이 닭이라는 것을 알아차리는 데 시간이 좀 걸렸습니다. 스웨덴 사람인 Ulf Norell이 만들었습니다.

옆에 있는 작은 표는 기본적으로 Agda가 어떻게 타입과 값의 구분을 모호하게 하려고 하는지 보여줍니다. Agda는 단순히 꽤 균일한 방식으로 사물을 던지지만, 일부 고급 언어에서는 각각이 고유한 구문적 요소로 취급됩니다. 실제로 동일한 것을 표현하는 방식이 다릅니다.

하지만 철학과 동기 부여에 대한 이야기는 이 정도로 마무리하겠습니다. 이제 Agda 코드를 보고 싶어 하실 거라고 생각합니다. 이것이 바로 제가 이러한 슬라이드를 통해 의도한 바입니다. 그럼 시작해 볼까요? 여기에 준비해 둔 몇 가지 모듈이 있습니다. 하나는 언어의 문법을 설명하는 것입니다. 타입, 함수 등을 정의하는 방법을 보여드리겠습니다. 그런 다음 타입으로서의 명제라는 개념에 대해 알아보겠습니다. 이 방에 계신 분들 중에 타입으로서의 명제가 무엇을 의미하는지 아시는 분이 계신가요? 아시는 분은 손을 들어주세요. 몇 분 계시네요. 좋습니다. 제가 여러분의 언어로 말하고 있는지 확인하고 싶었습니다. 그런 다음 몇 가지 기본적인 행렬 연산을 포함하는 매우 작은 행렬 라이브러리를 살펴보고 마지막으로 Agda의 탈출구 역할을 하는 Haskell FFI에 대해 알아보겠습니다. 그럼 시작해 보죠. 이것은 문법을 소개하는 첫 번째 모듈이고 몇 가지… 잠시 제 폰 도우미를 업데이트하겠습니다. Agda 모드에 대해 몇 가지 말씀드리겠습니다. 제 생각에 대부분의 Agda 프로그래머는 Emacs를 사용하는 것 같습니다. 저는 Emacs를 사용해 본 적이 없지만, 'Control-C Control-어쩌구'와 같은 명령이 많다고 합니다. 그리고 이것은 그냥... 무언가를 요청하는 명령입니다. 예, 감사합니다. 불을 좀 밝혀주시겠어요? 너무 어둡다는 의견이 있네요. 사실 저는 VS Code에서 그걸 어떻게 바꾸는지 모르겠습니다. '선호하는 밝은 색상'은 없습니다. 누군가 뭔가를 제안했는데... 'Command-K Command-T'인가요? 아, 좋습니다. 훨씬 보기 좋네요. 감사합니다. 글꼴 크기도 좀 키울 수 있을 것 같습니다. 마지막까지는 보이지 않겠지만요. 좋아요, 더 보기 좋나요? 좋습니다.

네, Agda 모드는 코드를 작성할 때 도움을 주는 여러 가지 명령어입니다. 이것들이 주요 명령어이고 저는... 바로 그 Conor McBride가 키보드 위에 카메라를 설치해서 어떤 명령어를 실행하는지 보여주는 기술을 사용할 것입니다. 여기에도 표시됩니다. 잘 보시면 제가 이러한 명령어를 실행할 때 확인하실 수 있을 것입니다. 하지만 네, 단일 모듈을 로드하고 타입 검사를 하고, 전체를 개선하는... Agda 프로그래밍과 테스트, REPL 작업의 99%가 여기서 이루어집니다. REPL과 동일한 환경입니다. 그리고 출력은 모두 이 작은 탭에 표시됩니다. 그럼 시작해 보죠. 먼저 몇 가지 타입과 값이 있습니다. 이것은 Haskell의 GADT 문법과 매우 유사합니다. 익숙하신 분들은 'data'라고 하면... 이것은 타입의 이름이고 저것은 타입의 타입입니다. 네, Agda에는 'kind'가 없습니다. 타입은 그냥 타입을 가집니다. '집합'이라고 불립니다. 왜냐하면 타입은 실제로 값의 모음일 뿐이기 때문입니다. 여기서 이 생성자는 3에서 3으로 가는 타입을 가지고 있습니다. 등등. 그리고 이것은 타입 3의 값의 예입니다. 그리고 또 다른 하나. Agda는 보시다시피 유니코드를 지원합니다. 이 작은 2… Agda는 유니코드를 매우 적극적으로 사용합니다. 매우 흔한 일이며 우리는 유니코드를 많이 사용할 것입니다. 하지만 이것은 타입 3의 두 가지 다른 값입니다. 이것이 합 타입을 정의하는 방법입니다. 여기에 Haskell의 'Either'와 동일한 것이 있습니다. 보시다시피, Haskell이나 Purescript, 또는 다른 방언을 보신 적이 있다면 이것은 매우 유사해 보입니다. 왼쪽에 타입이 있고 오른쪽에 타입이 있으며 'Either a' 또는 'b'를 얻는 방법은 두 가지입니다. 'Left' 주입을 수행하여 타입 'a'의 요소를 가져와서 타입 'Either a' 또는 'b'의 요소를 반환하거나, 오른쪽에서 수행할 수 있습니다. 그리고 여기에 'Either'의 값이 있습니다. 여기서 우리는 또 다른 문법 요소를 도입했습니다. 이것은 암시적 매개변수입니다. 따라서 이 값을 호출할 때, 이 값을 사용할 때, 우리는 일반적으로 타입 'a'가 무엇인지 말하고 싶지 않습니다. 문맥에서 분명할 것입니다. 하지만 실제로는 꽤 자주 이 인수를 제공해야 합니다. 따라서 이것은 'value of either'가 자연수 또는 모든 타입의 'Either' 타입을 가진다는 것을 말하고 있습니다. 왜냐하면 'Left 10'이기 때문입니다. 자연수...

그리고 여기에 곱 타입의 문법이 있습니다. 'record'라는 다른 키워드가 사용된 것을 알 수 있습니다. 그리고… 네, 그 이유는 곱 타입과 합 타입 사이에 근본적인 차이점이 있기 때문입니다. 서로 이중 관계입니다. 그리고 개인적으로는 레코드의 필드가 무엇인지, 곱 타입이 무엇인지 지정하는 작은 섹션이 있는 것이 보기 좋다고 생각합니다. 혹시 모르시는 분들을 위해 말씀드리자면, 두 가지는 동일합니다. 좋아하는 프로그래밍 언어로 레코드를 정의할 때마다 실제로는 곱 타입을 정의하는 것입니다. Agda는 이를 매우 명확하게 보여줍니다. 그리고 이러한 타입 중 하나를 빌드하기 위해 생성자를 제공할 수 있습니다. 여기서 사용되는 것을 볼 수 있습니다. 따라서 이것은 3의 값 하나와… 음… 6이라는 타입과 6의 값을 포함하는 쌍입니다. 생성자를 사용하여 빌드하기만 하면 됩니다.

여기에 Haskell의 튜플 타입 정의가 있습니다. 두 가지 다른 타입의 쌍입니다. 다시 말하지만, 두 가지 타입을 매개변수로 사용합니다. 하나는 첫 번째 필드에, 다른 하나는 두 번째 필드에 들어갑니다. 매우 간단합니다. 이것이 쌍을 구성하는 방법입니다. 쌍 생성자에 이름을 지정했기 때문에 Haskell과 달리 생성자를 대문자로 쓸 필요가 없는 것을 알 수 있습니다. 네, 매우 기본적인 내용입니다. 여기에 함수를 정의하는 방법의 예가 있습니다. 다시 말하지만 Haskell과 유사합니다. 두 자연수를 가져와서 더하는 함수와 인수 중 하나에 대해 패턴 매칭을 수행하는 함수가 있습니다. 따라서 3개 값 중 하나를 자연수에 더합니다. 따라서 값이 1이면 1을 더하고, 2이면 2를 더합니다. 등등. 그리고 이것은 여전히... Haskell과 매우 유사해 보입니다. 그렇죠? 그리고 꽤 멋진 몇 가지 문법적 요소를 더 살펴보겠습니다. Agda는 중위 연산자를 지원합니다. 따라서 이 함수의 이름은 꽤 이상하지만, 사용할 때는 의미가 있습니다. '첫 번째 인수를 두 번째 인수에 더하되, 무언가와 무언가가 참이면 그렇게 하고 그렇지 않으면 둘 중 하나를 선택합니다.' 따라서 4개의 인수를 사용합니다. 4개의 작은 밑줄입니다. 그리고 자연수를 반환합니다. 여기서 본문을 볼 수 있습니다.

let 바인딩은 Haskell과 동일하게 작동합니다. 따라서 '조건 1'과 '조건 2'를 수행합니다. 여기서는 부울 연산자입니다. 그리고 둘 다 참이면 합하고 그렇지 않으면 둘 중 하나를 선택합니다. 어떻게 선택할까요? where 블록에 정의된 이 함수를 사용합니다. 그리고 이 함수는 Agda에서 case와 같은 역할을 하는 with 키워드를 사용합니다. 그리고 이것은 실제로 의존 패턴 매칭입니다. 즉, with 내부의 표현식에 대해 패턴 매칭을 수행할 때 컴파일러는 패턴 매칭 본문에 있는 타입에 대해 알고 있습니다. 제 생각에는 with를 사용하는 예를 볼 수 있을 것 같습니다. 대부분의 경우에는 필요하지 않을 것 같습니다. 그리고 이 경우에는 이것은 의존적이지 않은 패턴 매칭입니다. 거짓이면 'm'을 반환하고 그렇지 않으면 'n'을 반환합니다. 하지만 네, 이렇게 생겼습니다. 자, 여기 값이 있습니다. 15를... 10을 5에 더하지만 true이고 5가 10보다 작을 때만 그렇게 하고 그렇지 않으면 둘 중 하나를 선택합니다. 이것은 15입니다. 그리고 여기에 숫자를 가져와서 15를 더하는 'add 15'가 있습니다. 이것은 람다 문법을 보여주기 위한 것입니다. 람다는 이렇게 멋진… 음… 유니코드 람다입니다. 실제 그리스 문자와 같습니다. 보기 좋다고 생각합니다. 따라서 Haskell에서 이것은… 음… 이 함수가 '자연수에서 자연수로' 가는 타입을 가지고 있다고 말하고 있습니다. 그리고 이 값은 '자연수에서 자연수로' 가는 타입의 무언가입니다. 이 값은 무엇일까요? 자연수를 가져오는 함수입니다. 음… Haskell에서처럼 이렇게 쓸 수도 있었을 것입니다. 네, 람다가 있습니다.

이제 타입으로서의 명제에 대해 알아보겠습니다. 왜냐하면 유용한 디팬던트 타입 프로그래밍을 하려면 이것을 이해해야 하기 때문입니다. 따라서 문법 모듈을 가져오겠습니다. import 이름 앞에 'open'이 있는 것을 보셨을 것입니다. 이것은 이 모듈의 모든 것을 범위로 가져와서 최상위 변수처럼 취급하라는 의미입니다. 여기… 모듈에서 항목을 숨길 수 있습니다. 따라서 여기서는 몇 가지 항목을 가져오고 있습니다. 최소한으로 유지하려고 노력했습니다. 표준 라이브러리에서 가져오는 항목은 이 정도입니다. 하지만 항목을 숨길 수 있습니다. 이름을 숨길 수 있습니다. 그리고 이제 실제로 디팬던트 타입에 대해 알아보겠습니다. 따라서 여기 이 타입은 동등 타입입니다. 그리고 이것은… 모든 타입… 집합에 대해… 그리고 'x'가 멤버인... 집합의 멤버인 모든 타입에 대해… 그리고 해당 타입의 모든 요소에 대해 이 타입의 요소를 제공하면 집합을 반환합니다. 좋아요.

그리고 이 타입의 유일한 구성원인 'refl'은… 'x'는 'x'와 같다는 타입을 가지고 있습니다. 따라서 이것은… 이 타입에 대해 패턴 매칭을 수행할 수 있는 유일한 방법, 이 타입으로 무언가를 할 수 있는 유일한 방법은 동일한 두 값이 있는 경우뿐이라는 것을 의미합니다. 좋아요. 따라서 여기 'x'는 이 생성자의 양쪽에 있습니다. 보이시나요? 여기에도 나타나고 여기에도 나타납니다. 콜론의 왼쪽에 나타나는 타입과 오른쪽에 나타나는 타입 사이에는 차이가 있습니다. 하지만 저는 그 부분에 대해서는 자세히 설명하지 않겠습니다. 제가 보여드리고 싶은 것은… 이것이 두 개의 매개변수를 사용하더라도 실제로 동일한 경우에만 값을 구성할 수 있다는 것입니다. 좋아요.

따라서 Agda는 타입 수준에서 이를 계산할 수 있습니다. 여기에 구멍이 있습니다. 이 모듈에서 'Control-C Control-L' 명령어를 실행한 첫 번째 결과입니다. 이것은 'hole0'이고 이 구멍은… '11 + 4'는 '15'와 같다는 타입을 가지고 있습니다. 이전에 정의한 값입니다. 이것의 타입입니다. 따라서 이것이 타입으로서의 명제가 '11 + 4는 15와 같다'는 명제를 표현하는 방법입니다. 타입… 제가 이것을 말하지 않은 이유는 다시 똑같은 말을 반복해야 하기 때문입니다. 하지만 둘은 동일합니다. 명제는 타입입니다. 그냥 그렇습니다. 이것은 논리학과 컴퓨터 과학의 기본적인 사실입니다. 따라서 이 타입의 구성원은 무엇일까요? 타입… 네, 이 두 값에 대한 '동등' 타입의 고유한 구성원입니다. 그리고 이제 저는 Agda가 이를 자동으로 해결하도록 매우 강력한 명령어인 'Control-C Control-A'를 사용하겠습니다. Agda는 이 명제의 증명이 이 타입의 값이라는 것을 알아낼 수 있습니다.

이것이 바로 대응 관계입니다. 명제는 타입이고 증명은 값 또는 프로그램입니다. 타입의 값은 해당 타입이 참이라는 증거입니다. 곧 이에 대한 몇 가지 예를 더 살펴보겠습니다. '1 + 13'이 '15'와 같다는 것을 증명하고 싶다면… 그것은 불가능합니다. 이 점에 대해서는 여러분을 굳이 설득할 필요가 없을 것 같습니다. 하지만 제가… 이제 여기서 문맥을 보여주는 명령어를 사용하겠습니다. 제가 보여드리려는 것은… 이것이 우리가 보는 출력입니다. 컴퓨터 숫자 14가 컴퓨터 숫자… 15와 같다는 것을 보여드리려고 합니다. 실제로는 보여줄 수 없습니다. 곧 문맥을 사용하는 몇 가지 예를 더 살펴보겠습니다. 충분합니다. 따라서 타입으로 다른 관계를 정의할 수 있습니다. 예를 들어 숫자가 다른 숫자보다 작거나 같다는 것, 또는 실제로 무엇이든… 네, 모든 명제… 하지만 이를 생각하는 또 다른 방법이 있습니다. 타입이 참이면 구성원이 있습니다. 적어도 하나의 값이 있습니다. 적어도 하나의 요소가 있는 집합입니다. 구성원이 없으면 아무것도 없습니다.

그리고 이 두 가지 기본적인 참 또는 거짓 상태는 이 두 가지 타입으로 표현됩니다. 하나는 ⊥(bottom)이라고 하고 다른 하나는 ⊤(top)이라고 합니다. 좋아요. 무서운 소리네요. 화재 경보인가요? 좋아요. 이제 훨씬 덜 무섭네요. 네, 따라서 이 두 가지 타입은 각각 구성원이 없고 하나의 요소로 구성됩니다. 하지만 ⊥는 분명한 이유로 거짓이라고도 합니다. 근본적으로 거짓인 명제를 나타냅니다. 그리고 ⊤는 참이라고 합니다. ⊤는 'tt'라는 단일 구성원을 가지고 있으며, 이 값은 ⊤ 타입으로 표현되는 명제가 참이라는 증거입니다. 따라서 이제 의존 함수를 사용하여 이러한 타입을 기반으로 관계를 정의할 수 있습니다. 이것을 보세요. 이것은 두 자연수를 가져와서 집합을 반환하는 함수입니다. 타입을 반환합니다. 좋아요. 그리고 이것의 논리를 생각해 보겠습니다. 0이 'n'보다 작거나 같으면… 첫 번째 인수에 대해 패턴 매칭을 수행하면 참이라는 것을 알 수 있습니다. 0은 다른 모든 자연수보다 작거나 같습니다. 따라서 ⊤ 타입으로 표현합니다. 그리고… 네, 이것은 구멍이었어야 했는데... 이제 다른 구멍을 채워보겠습니다. 이 경우는 어떨까요? 숫자의 후속자가 있는 경우… 음… 피아노… 이걸 물어봤어야 했는데… 자연수의 피아노 표현은 0은 자연수이고 자연수의 후속자는 자연수라는 것입니다. 이것은 귀납적 정의이며 여기서 패턴 매칭을 수행하는 것입니다. 따라서 자연수의 후속자… 자연수가 될 수 있는 가장 작은 수는 0이므로 왼쪽의 것은 적어도 1이고 1 또는 1보다 큰 수는 0보다 작거나 같지 않습니다. 따라서 이것은 ⊥ 타입입니다. 이것이 바로 우리가 표현하려는 것입니다. 이것이 우리가 정의하는 관계입니다. 그리고 타입...

그리고 두 자연수가 모두 무언가의 후속자인 경우는 어떨까요? 네, 왼쪽의 것이 오른쪽보다 작거나 같으려면 둘의 전임자가 오른쪽보다 작거나 같아야 합니다. 따라서 이것은… 모니터가 느리네요. 이것은… 이렇게 됩니다. 관계를 재귀적으로 호출하고 있습니다. 그리고 여기서 이것이 작동한다는 작은 증명을 할 수 있습니다. 네, 0이… 100보다 작거나 같다는 것을 예상해야 합니다. 그리고 우리의 목표가 무엇인지, 이것이 참이라는 증거를 제공하기 위해 무엇을 제공해야 하는지 알 수 있습니다. ⊤ 타입입니다. ⊤ 타입에는 단 하나의 구성원이 있습니다. Agda에게 타입의 값을 제공하도록 요청할 수 있는지 궁금하네요. 음… ⊤ 타입… 물론 가능합니다. 구성원이 하나뿐이기 때문에 Agda는 타입을 보고 이것이 참이라는 것을 알 수 있습니다. 또는… 무엇을… 무엇을… 타입을 계산한 다음 '좋아요, 이것이 제공해야 하는 것입니다. 이것이 제공해야 하는 증거입니다'라고 말합니다. 그리고 증거는 사소합니다.

우리는 엄격한 부등식도 가지고 있습니다. 따라서 여기서 우리는 0이 0보다 작지 않다는 것을 말하고 싶습니다. 이번에는… 여기에 ⊥가 있습니다. 음… 이것도 분명히 거짓입니다. 다른 모든 것보다 크거나 같은 것은 분명히 0보다 작지 않습니다. 하지만 0은 모든 후속자보다 작거나 같습니다. 따라서 이것은 ⊤가 될 것입니다. 그리고… 마지막 경우에 대한 재귀 호출입니다. 또한 저에게는 치트 시트가 있습니다. 아시다시피 라이브 코딩은 어렵습니다. 음… 그리고 사실 생각보다 진행 속도가 느려서… 음… 타입으로서의 명제 모듈의 후반부는 구멍을 해제하고 코드를 살펴보는 방식으로 빠르게 진행하겠습니다. 왜냐하면 시간이 부족하기 때문입니다. 다룰 내용이 꽤 많습니다. 따라서 이것은 무엇을 말하는 것일까요? 타입… 타입 안전 뺄셈… 'm'보다 작은 'n'은… 'n'이… 'm'보다 작다는 증거를 제공하는 경우에만 또 다른 자연수를 제공합니다. 그리고 여기에 Agda가 하는 일이 있습니다. 오른쪽에 0이 있으면 이미… 음… 왼쪽의 것이 오른쪽보다 크거나 같다는 것을 이미 알고 있기 때문에 'tt' 값을 제공할 수 있습니다. 미리 계산했습니다. 따라서 'm'에서 0을 뺀 것은… 분명히 'm'입니다. 이제 'm'에서 무언가의 후속자를 뺀 경우… 이것은 무엇이 되어야 할까요? 네, 이것이 참이라는 증거를 제공할 수 없습니다. 이 방정식의 이 부분에 대한 증거를 제공할 수 없습니다. 그리고 이것에 대한 증거가 있다면 ⊥ 타입의 구성원을 갖게 될 것이고, 그것은 존재하지 않습니다. 따라서 이를 표현하는 방법은 여기 이 빈 괄호입니다. Haskell이나 그와 같은 것의 unit이 아닙니다. 음… 그리고 무언가의 후속자에서 무언가의 후속자를 빼고 왼쪽이 오른쪽보다 크다는 증거가 있다면… 음… 재귀적으로 뺄셈 함수를 호출하여… 음… 이 숫자의 전임자를 제거합니다. 따라서 여기서 우리의 뺄셈이 정확한지 테스트할 수 있습니다. 뺄셈 함수... 그리고 예상하셨겠지만, Agda는 이를 자동으로 계산할 것입니다. 타입을 보고 방정식의 양쪽이… 동일하다는 것을 알 수 있습니다. 그리고 이것이 기본적으로 타입으로서의 명제의 개념입니다. 더 고급 증명을 할 수도 있지만, 저는 디팬던트 타입으로 프로그래밍하는 부분을 다루고 싶습니다. 따라서 여기서 조금 조금 더 빠르게 진행하겠습니다. 이것은 디팬던트 타입의 전형적인 예입니다. 컴파일 타임에 벡터의 길이를 알 수 있는 벡터입니다. 물론 미리 알 수 있다는 의미는 아닙니다. 사용자 입력 등을 받을 수 있지만, 요점은 타입의 일부라는 것입니다. Haskell이나 다른 언어의 벡터... 네, 대부분의 언어에서는 일반적으로 벡터는 다른 타입을 포함할 뿐입니다. 타입 자체에 길이가 연결되어 있지 않습니다. 하지만 이 경우에는 'Vec'입니다. 이 타입은 어떻게 정의될까요? 길이가 0인 'Nil' 벡터가 있고 'Cons' 벡터가 있습니다. 이 생성자는 요소를 가져오고 다른 벡터를 가져와서 해당 타입의 요소가 그만큼 있는 벡터를 반환합니다. 더하기 1. 받은 첫 번째 요소를 앞에 붙이기만 하면 됩니다. 그리고 여기에… 이제 줄 바꿈이… 단어 줄 바꿈을 전환할 수 있습니다. 네, 그렇게 하면 아무것도 놓치지 않을 것입니다. 여기에 'take' 함수가 있습니다. 저는… 음… 이것을 채우는 대신 치트 시트를 사용하겠습니다. 이런… 'take' 함수는… 음… 숫자를 제공하고 벡터를 제공하면 앞에서부터 해당 개수만큼 요소를 가져온 벡터를 반환합니다. 하지만 이 경우에는 제공하는 숫자가 벡터의 길이보다 작다는 증명을 제공해야 합니다. 숫자 'a'를 제공하고 'a'가 길이보다 작다는 증명을 제공하면 첫 번째 벡터에서 가져온 길이 'a'의 벡터를 제공합니다. Haskell에서 이것을 본 적이 있을 수도 있습니다. 여기에는 특별한 것이 없습니다. 0을 가져오면 빈 벡터를 반환합니다. 무언가의 후속자를 가져오면… 음… 요소를 하나 가져와서 벡터의 뒤로 이동합니다. 여기에 두 벡터를 연결하는 것이 있습니다. 음… 치트 시트를 사용하겠습니다. 빈 벡터가 있으면 실제로는 빈 벡터를 두 번째 벡터와 연결하는 것이므로 두 번째 벡터를 반환하기만 하면 됩니다. 음… 반면에 첫 번째 벡터에 무언가가 있으면 그것을 순회하고 나머지를 연결한 결과 앞에 놓습니다. 여기에 벡터에서 요소를 가져오는 것이 있습니다. 다시 말하지만 벡터의 길이가 있고… 아… 'wp'라는 단어는 좀 안 좋은 생각이었던 것 같지만, 여기서 아이디어를 얻을 수 있습니다. 찾고 있는 인덱스가 길이보다 작다는 증명이 있습니다. 해당 요소의 무언가를 얻을 수 있습니다. 'take'와 매우 유사한 아이디어입니다. 싱글톤을 구성합니다. 싱글톤을 잘 활용하고 있습니다. 음… 중위 연산자... 여기에 요소를 제공하면 해당 요소가 있는 길이 1의 벡터를 반환합니다. 음… 여기에 우리의… 오른쪽 인덱스가 작동한다는 작은 증명이 있습니다. 자동 해결… 아기… Agda는 알고 있습니다. 'v' 벡터에서 인덱스 2를 찾는다는 타입을 지정합니다. 여기서 바인딩한 'v'입니다. 네, 타입에 let 바인딩이 있는데, 제 생각에는 정말 멋진 기능입니다. 음… 그것은 6과 같습니다. 네, 물론입니다. 그리고 몇 가지 일반적인 고차 함수... 네, 'map'... 'map'을 좋아하지 않는 사람이 있을까요? 함수를 벡터에 적용하고 벡터의 나머지 부분을 순회하면서 함수를 적용합니다. 여기에 지점별 적용이 있습니다. 함수가 있고 길이가 'n'인 벡터가 있습니다. 이 벡터는 'a'에서 'b'로 가는 함수를 포함합니다. 그리고 'a'의 벡터를 제공하면 'b'의 벡터를 얻을 것으로 예상합니다. 이것은… 음… 매우 일반적인 고차 함수는 아닙니다. 적용 가능한 펑터를 떠올리게 할 것입니다. 하지만 곧 사용할 것이기 때문에 여기에 포함했습니다. 또한 'replicate'를 사용할 것입니다. 'replicate'는 요소를 제공하면 길이가 'n'인 벡터를 제공합니다. 'n'이 무엇이든... 'n'은 여기서 암시적 인수로 제공됩니다. 하지만… 'n'이 0일 때… 다시 말하지만, 같은 아이디어입니다. 'n'이 z... 빈 벡터를 반환합니다. 그리고 'n'이 무언가의 후속자인 경우… 앞에 놓습니다. 음… 복제… 즉, 꼬리에 대해 동일한 함수를 호출합니다. 여기에 전치가 있습니다. 벡터의 벡터가 있는 경우 기본적으로 열과 역할을 바꿔야 합니다. 여기서는 지점별 적용을 영리하게 사용하고 있기 때문에… 음… 필요했습니다. 네, 아쉽게도 전치에 대해 설명할 시간이 없지만, 이 코드를 자세히 살펴보고 왜 작동하는지 확인하거나 모든 타입 'a'와 'a'의 1, 2, 3 요소에 대해 작동한다는 증명을 작성할 수 있습니다. 이 행렬을 전치하면 이 행렬이 됩니다. 1 1 1, 2 2 2, 3 3 3. 1 1 1, 2 2 2, 3 3 3. 이것을 어떻게 해결할까요? 해결되었습니다. 모든 타입과 이 타입의 3가지 구성원에 대해 해결되었습니다. 여기에 마지막 고차 함수가 있습니다. 'zipWith'... 'zipWith'를 모르신다면… 두 개의 벡터와 두 개의 인수를 사용하는 함수를 사용하여 해당 함수를 두 벡터에 적용합니다. 그래서 'zip'입니다. 'zip'은 바지의 지퍼와 같고 두 개의 가닥에서 하나의 것을 얻습니다. 음… 몇 가지 디팬던트 타입을 더 살펴보겠습니다. 이제 진짜가 나타납니다. 이것은 시그마 타입이라고 합니다. 여기 이 글자… 타입 'a'의 무언가와 'a'의 요소에서 집합으로 가는 함수를 제공하면 집합을 반환합니다. 따라서 이것의 필드는… 첫 번째 필드는 타입 'a'를 가지고 있고 두 번째 필드는 첫 번째 필드에 적용된 함수… 즉, 첫 번째 필드의 요소에 적용된 함수를 가지고 있습니다. 무엇이든… 그리고 이 의존적인… 시그마 타입을 의존 곱이라고 부르는 이유는… 쌍이기 때문입니다. 항상 두 개의 값을 가지고 있습니다. 'proj₁'과 'proj₂'. 단, 두 번째 쌍의 타입… 두 번째… 요소의 타입은 첫 번째… 요소의 값에 따라 달라집니다. 그리고 여기에 그 예가 있습니다. 따라서 이것은 'n if false list of tt if true'라는 함수입니다. 부울을 가져와서 집합을 반환합니다. 'b'에 대해 패턴 매칭을 수행합니다. 거짓이면 자연수 타입을 반환하고 참이면 모든 자연수 'n'에 대해 'tt'의 'Vec'를 반환합니다. 그리고 여기에 이 함수를 사용하는 의존 곱의 값이 있습니다. 따라서 이것은 부울과 이 함수의 곱입니다. 두 번째 매개변수입니다. 따라서 이 함수는… 네, 두 번째 값의 타입은 무엇이 되어야 할까요? 첫 번째 값은 거짓이므로 자연수가 되어야 합니다. 그래서 이것이 컴파일됩니다. 두 번째 예는… 네, 이것은 'true true'이므로 두 번째 것의 타입은 이 'tt'의 목록입니다. 3개의 'tt'. 왜 이것을 사용해야 하는지 모르겠지만, 값에 따라 달라지는… 곱 타입을 가질 수 있다는 것을 보여주기 위한 것입니다. 음… 표현식과 타입 시그니처를 가질 수 있습니다. 이제 정말 빨리 진행해야 합니다. 음… 하지만 이것은 정말 대단합니다. 이것으로 많은 것을 할 수 있습니다. 여기에 5보다 큰 자연수 집합의 타입이 있습니다. 첫 번째 요소에 대한 증명인 두 번째 요소가 있는 의존 곱으로 정의하기만 하면 됩니다. 음… 그리고 값 7이 5보다 크다는 증명을 구성할 수 있습니다. 증명은 'tt'가 될 것입니다. 왜냐하면 타입에서 계산되기 때문입니다. 음… 하지만 첫 번째 요소가 3인 'greaterThan5'의 값을 생성할 수 없습니다. 이 구멍의 타입은 ⊥가 될 것입니다. ⊥의 값을 생성하는 것은 불가능합니다. 음… 자연수에 대해 매개변수화할 수 있습니다. 따라서 여기에 'greaterThan n'이 있습니다. 값 'n'이 있습니다. 'greaterThan7' 타입입니다. 물론… 그렇습니다. 좋아요, 아직까지는 잘 따라오고 계신가요? 다룰 내용이 꽤 많기 때문에 마지막 부분은 빠르게 진행해야 합니다. 프로그램… 간단한 프로그램이지만… 그래도… 음… 작은 행렬 라이브러리를 작성하는 모듈을 살펴보겠습니다. 자연수를 사용하고 이전에… 이전에 정의한 것을 사용하고 있습니다. 여기서 'Num'이라는 레코드를 정의할 것입니다. 집합을 가져와서 집합을 반환합니다. 이 집합에 대한 함수인 몇 가지 필드가 있습니다. 일부는 값이지만… 음… 이것은 함수형 프로그래밍이므로 함수는 그냥… 값입니다. 음… 그리고 이것은 Agda의… Agda의… Haskell의 타입 클래스에 대한 답변입니다. 혹시 모르시는 분들을 위해 말씀드리자면, Haskell의 타입 클래스… 음… 런타임에… 이 타입에 대한… 딕셔너리로 축소됩니다. 이 함수의 구현은 이 타입에 대한 것입니다. 이 함수의 구현은 저 타입에 대한 것입니다. Agda는 이를 훨씬 더 명확하게 만듭니다. 음… 이것은 모듈의 나머지 부분에서 이 레코드의 멤버를 범위로 가져오는 문법입니다. 여기에 인스턴스를 선언하는 방법이 있습니다. 인스턴스는 그냥… 이 레코드의 값입니다. 'Num'... 'Num'... 네, 이 집합, 자연수 집합에 대한 레코드의 모든 필드를 정의합니다. 그리고 이 집합, 실수 집합에 대한… 여기서 레코드를 만드는 문법은 코패턴이라고 합니다. 재밌는 표현이라고 생각합니다. 기본적으로 레코드의 타입을 제공하고… 그리고… 이 함수를 이 레코드에 적용한 것이 무엇인지 말합니다. 음… 코패턴이라고 부르는 이유는 패턴… 패턴을 매칭할 때 패턴을 해체하여 '이 분기에 대해 이것을 수행합니다'라고 말하는 반면, 코패턴에서는 '모든 가능한 각도에서 이것을 구성하는 방법은 다음과 같습니다'라고 말합니다. 따라서… 음… 음… 설명하기가 좀 어렵지만… 음… 기본적으로 필드를 기반으로 무언가를 구성하는 방법과 무엇이 될 수 있는지에 따라 무언가를 해체하는 방법입니다. 이중… 코패턴… 범주론… 하하… 네… 음… 그리고 이것이 인스턴스 인수임을 나타내는 방법입니다. 인스턴스 인수로 사용할 수 있습니다. 음… 'instance'라는 키워드를 앞에 붙이기만 하면 됩니다. 음… 그럼 행렬 타입과 행렬에 대한 함수를 살펴보겠습니다. 기본적으로 벡터의 벡터에 대한 새 타입입니다. 행의 개수와 열의 개수가 있습니다. 음… 그리고 모든 타입… 에 대해… 음… 그리고 두 행렬을 더할 수 있습니다. 치수가 같으면… 이것이 바로 이 함수가 정의하는 것입니다. 다시 말하지만 중위 연산자입니다. 따라서 두 행렬을 더하는 방법은… 네, 첫 번째 벡터를 첫 번째 벡터 레이어와 'zipWith'하고 두 번째 벡터를 'zipWith'하고 도중에 찾은 것을 더합니다. 이것이 바로 이 중첩된 'zipWith'가 하는 일입니다. 두 행렬에 적용합니다. 음… 줄 바꿈이… 단어 줄 바꿈을 전환했었는데… 네… 그렇습니다. 음… 따라서 'a'의 행렬을 제공하면… 'a'의 다른 행렬을 제공하면… 'a'의 또 다른 행렬을 제공합니다. 같은… 치수를 가진… 행렬을 곱하는 것이 더 흥미롭습니다. 음… 이제는… 치수가 'r'과 'c'인 행렬과 치수가 'c'와 'p'인 행렬을 곱하여 치수가 'r'과 'p'인 행렬을 생성할 수 있다고 말합니다. 매우 자연스럽게 표현됩니다. 음… 구현 세부 사항에 대해서는 자세히 설명하지 않겠지만, 녹화를 다시 보고 코드를 자세히 살펴보면서 작동하는지 확인할 수 있습니다. 음… 아… 이 코드를 자세히 살펴보라고 이미 말씀드렸네요. 왜냐하면 벡터에 대해 정의한 전치를 사용하고 있기 때문입니다. 음… 따라서 실제로는 두 개의 코드 레이어를 자세히 살펴봐야 합니다. 여기에 몇 가지 다른 함수가 있습니다. 그냥… 음… 벡터를 제공하면 열 행렬을 구성합니다. 즉, 단일 열이 있는 행렬입니다. 따라서 'n'... 행이 있습니다. 벡터의 길이이고 열은 1개입니다. 그리고 행렬에 대한 벡터… 행은… 음… 행이 1개이고 열이 있습니다. 그리고 이것은 전치의 동의어일 뿐입니다. 하지만 수학 표기법으로 작성된 행렬을 본 적이 있다면… 음… 'T' 제곱이 있습니다. 음… 깔끔하네요. 음… 네, 이러한 중위 선언이 곳곳에 있습니다. 이것은 연산자가 왼쪽으로 결합할지 오른쪽으로 결합할지 나타냅니다. 이 경우에는 인수가 하나이므로 의미가 없습니다. 음… 그리고 우선순위와 얼마나 밀접하게 결합해야 하는지… 네, 작은 행렬 라이브러리입니다. 행렬을 더하고 곱하고 벡터로 변환할 수 있습니다. 간단한 것들입니다. 그리고 행렬의 의사 역행렬을 구하고 싶습니다. 이제 이것은 까다로운 연산입니다. 행렬을 역행렬로 바꿔본 적이 있다면 LU 분해와… 음… 행렬이 특이 행렬이 아님을 확인하는 것이 간단한 알고리즘이 아니라는 것을 알 것입니다. 따라서… 음… 린디 효과로 돌아가서… Agda는 코드를 얼마나 신뢰할 수 있는지, 즉 코드가 정확한지 여부에 신경 쓰는지 여부에 따라 린디 효과를 활용할 수 있는 방법을 제공합니다. 오랫동안 사용되어 온 코드를 사용하고 정확하다고 믿을 수 있습니다. FFI를 사용하면... Agda는 Haskell로 컴파일됩니다. 음… 이것이 Agda가 궁극적으로 실행되는 방식이고 우리가 사용할 수 있도록 화면에 무언가를 생성하는 방식입니다. 그리고 Agda에는 FFI가 있기 때문에 Agda에서 Haskell 코드를 호출할 수 있습니다. 또한 Haskell에서 Agda 코드를 호출할 수도 있습니다. 흥미롭습니다. 음… 그리고… 음… 이 부분에 대해서는 딱히 할 말이 없습니다. 'trustMe'가 사용되는 것을 볼 수 있을 것이고, 이것은 바로… 네… '모든 타입 안전성은 잊어버리고 저를 믿으세요. 이것은 작동합니다.'라는 지점입니다. 참고로 이것은 실제 라이브러리 이름입니다. 패키지 이름입니다. 'trustMe'라고 합니다. 그리고 거기에 모든 것이 다른 모든 것과 같다는 증명이 있습니다. 저를 믿으세요. 정확합니다. 음… 따라서 이것이 작동하는 방식입니다. 아… 단어 줄 바꿈을 다시 설정해야겠네요. 네… FFI를 사용하기 위한 프라그마에는 세 가지 유형이 있습니다. 따라서 이것은 컴파일러에게… 음… 코드의 이 부분을 컴파일할 때 이 Haskell 코드를 삽입하라고 지시합니다. 'HSMatrix'를 가져옵니다. 그것은 무엇일까요? 여기 또 다른 프라그마가 있습니다. 'compile' 프라그마… 이 'postulate'... 논리학에서 'postulate'는 우리가 그냥… 사실이라고 말하는 것입니다. '이 명제를 가정해 보겠습니다.' 음… 'postulate'는… 음… 공리와… 음… 그냥… 사실이기 때문에 사실인 것들의 자리를… 음… 차지하려고 합니다. 제 생각에는 'postulate'와 공리 사이에 차이가 있는 것 같은데, 저는 잘 모르겠습니다. 하지만 Agda에서 아무것도 없는 상태에서 무언가를 만들어내는 방법입니다. 그리고 이것이… 음… FFI에 지시하는 내용입니다. 음… 실수의 목록의 목록을 가져와서 실수의 목록을 반환하는 이 'postulate'가 보이면 'invertMatrixAsList'로 설정합니다. 이것은 Haskell 코드입니다. 이것이 실제로 변환될 것입니다. 이것을 컴파일하는 대신… 음… 보일 때마다 이 Haskell 코드와 같게 만듭니다. 여기에는 목록을 벡터로, 벡터를 목록으로 변환하는 몇 가지 변환 코드가 있습니다. 음… 이 부분을 제외하고는 모두 건너뛰어야 할 것 같습니다. 여기 'trustMe' 증명… 네, 걱정하지 마세요. 저는… 이것은 작동할 것입니다. 저를 믿으세요. 저는 그 이름이 정말 마음에 듭니다. 음… 따라서 'postulate'를 호출하기 위해 'fromListOfLists'를 사용합니다. 음… 이것은 '-1' 제곱인 역행렬 연산자입니다. 먼저 변환 함수를 사용하여 행렬을 목록으로 변환한 다음… 음… 역행렬로 바꿉니다. 'postulate'를 호출하여 역행렬로 바꿉니다. 그런 다음 'trustMe'를 다시 전달하여 얻은 것을 변환하여… 음… 치수가 일치하는지 확인합니다. 따라서… 음… 모든 'n'에 대해 정사각형 행렬을 제공하면… 치수가 'n' 곱하기 'n'인 행렬을 제공하면 'n' 곱하기 'n'을 반환합니다. 따라서 이제 Agda 함수입니다. 이것은 그냥… Agda 수준에서 작동합니다. 증명은… 음… 또는 항은… 음… 'n'이… 행렬이 정사각형이고 입력이 출력과 같다는… 음… 증명에 대해 테스트될 것입니다. 등등. 그리고 여기에 행렬을 표시하는 몇 가지 코드가 있습니다. 다시 말하지만, 표준 라이브러리를 사용하고 있습니다. 음… 네, 그냥… 별거 없습니다. 벡터를 재귀적으로 순회하고 쉼표로 구분합니다. Haskell과 매우 유사해 보일 것입니다. 그리고… 음… 행렬을 표시하려면 'showVec'를 사용하기만 하면 됩니다. 마지막으로 살펴볼 모듈은… 메인 모듈입니다. 예! 이제 프로세서를 워밍업하는 것이 아니라 실제로 무언가를 실행하고 있습니다. 음… 여기에서 몇 가지 가져오기를 수행합니다. 음… Agda와 IO의 관계는 예상대로… 복잡합니다. 음… 여기 이 'level0'과 같은… 음… 몇 가지 문법적인… 문법적인 것뿐만 아니라 몇 가지 노이즈가 있습니다. 이미 IO를 실행하고 있음에도 불구하고 IO 호출을 실행해야 한다는 사실… 무슨 일이 일어나고 있는 걸까요? 너무 신경 쓰지 마세요. 음… 실제로는 이 'io.run'이나… 음… 레벨… 레벨 호출을 보지 말아야 합니다. 이것은 행렬을 출력하는 IO 호출일 뿐입니다. 행렬을 제공하면 ⊤를 반환하는 IO 연산을 제공합니다. 음… 그리고 여기에 메인 함수가 있습니다. 행렬 'm'을… 이 행렬, 2 6 3… 4로 설정합니다. 음… 'm⁻¹'을 역행렬로 설정합니다. 그리고… 음… 네, 여기서 볼 수 있는 것은… 먼저 행렬을 출력하고… 그 다음 역행렬을 출력하고… 그 다음… 음… 행렬과 역행렬을 곱한 것을 출력합니다. 그리고 이것은 단위 행렬을 반환해야 합니다. 음… 운이 좋다면요. 따라서 여기에 작은 빌드 명령이 있습니다. 이것은… 음… Nick의 셸 스크립트로 생성되었습니다. 코드를 컴파일하고… 음… 연결합니다. 그리고 이 코드를 실행할 수 있습니다. 그리고… 여기 있습니다. 행렬 'm'은 2 6 3 4이고 역행렬은 -0.4… 등등… 그리고 역행렬을 곱하면… 이런… 세상에… 맞았나요? 네, 따라서 여기에 1과 0.4가 있고… 음… 10의 -16제곱과… 10의 -16제곱… 그리고 1. 따라서 이것은 실제로 부동 소수점 오류를 뺀 1 0 0 1입니다. 단위 행렬입니다. 그리고… 네, 이것은… 음… 기본적으로 내용입니다. 여기에 작은 부록을 추가하여 Haskell 모듈이 어떻게 생겼는지 보여드리겠습니다. 그리고 여기 있습니다. 음… 실제로는 Singletons를 사용하지 않습니다. 이것은 다음 강연에서 다루겠습니다. 음… 하지만 이것은 외부 라이브러리를 사용하고 있습니다. 음… 이 Haskell 파일은… 음… Hackage에서 가져온 외부 라이브러리를 사용하고 있습니다. 'hmatrix'라고 합니다. 그리고 이 라이브러리는 의사 역행렬 알고리즘을 구현합니다. 이것이 바로 코드의 린디 부분입니다. 해당 코드는 공개되어 있고 테스트를 거쳤으며 오랫동안 실행되어 왔습니다. 음… 더… 네, lapack과 blas와 같은 더 잘 테스트된 코드에 의존합니다. 알고리즘… 음… 그리고 여기 이 작은 모듈은… 음… 오랫동안 사용되어 온 린디 코드를 신뢰하는 세계와… 음… fum... 매우 타입 안전한 Agda의 정리… 정리로 가득 찬 세계를 연결하는 역할을 합니다. 음… 그리고… 음… 제가 마지막으로 말씀드리고 싶은 것은… 음… 정확성을 표현하는 것이 편리할수록… 즉, 해당 타입에서 본 많은 것들이 매우 자연스럽습니다. '15는 11 + 4와 같습니다.' 누구나 해당 코드를 읽고 이해할 수 있습니다. 정확성을 표현하는 것이 편리할수록… 제 생각에는 편의성과 정확성 사이의 트레이드오프가 더욱 무의미해집니다. 즉, 의도를 컴퓨터가 검증 가능한 정확한 것으로 변환하는 데 드는 노력이 줄어듭니다. '이것이 정확한지 확인하기 위해 몇 개의 테스트 레이어와 얼마나 많은 타입 푸를 사용해야 할까?'라고 걱정할 필요가 줄어듭니다. 음… 그리고 제 생각에는 Agda가 여기서 중요한 역할을 합니다. 왜냐하면… 음… 제 생각에는… 음… 코드를 작성할 때 우리가 실제로 의미하는 바를 자연스럽게 표현할 수 있게 해주는 매우 아름다운 언어이기 때문입니다. 저는 그 단어를 신중하게 사용하고 있습니다. 그리고 제가 여러분을 설득했거나 적어도… 음… 그럴듯하게 들리도록 만들었기를 바랍니다. 이것으로 Agda 소개를 마치겠습니다. 감사합니다.

다시 한번 감사합니다, Andrea. 네, 저는… 모든 것을 이해하지는 못했습니다. 노력했습니다. 두 번 봤는데… 네… 질문 있으신가요? 네, 질문이 있습니다. 마이크를 전달해 주세요.

행렬에 요소를 잘못된 위치에 추가하면 타입이 어떻게 되는지 보여주시겠어요? 네, 물론입니다. 음… 마이크가 엉켰네요. 네, 보여드리겠습니다. 음… 전치의… 전치 증명에서 말씀하시는 건가요? 아니면… 음… 제공하려고 할 때… 네, 어떨까요? 만약… 만약… 아… 네, 좋은 질문입니다. 여기에 요소를 추가하면 어떻게 될까요? 네, 네. 따라서 타입 오류가 어떻게 표시되는지… 따라서 여기서… 음… 잘못 구성된 행렬을 추가했습니다. 행 중 하나에 열이 2개 있고 다른 행에는 열이 3개 있습니다. 따라서 이 모듈을 로드하려고 하면… 음… 네, 이미 무엇을 찾고 있는지 알고 있지 않으면 읽기가 좀 어렵지만, 기본적으로 진실을 말하고 있습니다. 무언가의 후속자는… 음… 0과 같지 않습니다. 음… 이 값을 구성할 때… 첫 번째 벡터의 패턴 매칭에 도달하면 매칭의 양쪽이 0인지 확인하려고 하고 둘 중 하나는… 음… 무언가의 'Succ'이 될 것이고, 'Succ'은 0이 아닙니다. 음… 하지만… 음… 네, 더 나은… 음… 타입 오류는… 음… 이렇게 하면 나타날 것입니다. 왜냐하면… 이런… 따라서 이것은 잘 구성된 행렬이지만… 정사각형이 아닙니다. 따라서 이제… 이제 훨씬 더 나은 오류입니다. '3은 2와 같지 않습니다.' 표현식 'Matrix Float'를 확인하고 있습니다. 음… 이것들을 제대로 가져왔다면 조금 더 보기 좋았을 것입니다. 음… 하지만 '3은 2와 같지 않습니다.' 왜냐하면 행은 2개이지만 열은 3개이기 때문입니다. 따라서… 음… 행렬이 정사각형이 아니기 때문에… 음… 역행렬로 바꿀 수 없습니다. 감사합니다.

다른 질문 있으신가요? 모두 이해하셨나요? 네, 혼자셨네요. 네, 죄송합니다. 아, 저쪽에 질문이 있네요. 네, 마이크를 전달해 드리겠습니다. 네, 발표 잘 들었습니다. 매우 흥미로웠습니다. 음… 질문은… 음… 좀 이상하게 들릴 수도 있지만… 음… 이런 유형의… 프로그래밍의 적용… 즉… 음… 실제로 이러한 기술을 사용해야 할… 수요가 있는 곳이… 네, 좋은 질문입니다. 그리고 Agda를 구체적으로 사용하는 회사는 적어도 한 곳 알고 있습니다. IOHK라는 회사인데, 지금은 IOG로 이름을 바꿨습니다. 블록체인을 하고 있고… 음… 블록체인 간의 프로토콜을 만들고 있습니다. 따라서… 음… 작성하는 코드가 정확해야 하고 Agda를 사용하여 정리를 증명합니다. 하지만 저는 Agda를 사용하여 개발된 프로그램을 알고 있습니다. 예를 들어 검증된 C 컴파일러가 Agda를 사용하여 개발되었다고 확신합니다. 그리고 그것은… 음… 'CompCert'라고 합니다. 제 생각에는 항공 소프트웨어와 같은 몇 가지 중요한 애플리케이션에서 사용됩니다. 오류가 발생하면 사람이 죽을 수 있습니다. 음… 네, 두 번째 부분은 확실하지 않지만… 음… 90% 확신합니다. Agda… 와 관련된 것입니다. 네, 좋아요. 저도 질문이 하나 있습니다. 어떻게 Agda를 접하게 되었나요? 네… 음… Agda를 접하게 된 계기는 Haskell에 관심이 있었고… 음… 석사 학위를… 복잡 적응 시스템으로 하고 있었습니다. 이것은… 음… 물리학과 컴퓨터 과학이 혼합된 분야인데… 음… 제 생각에는… 음… 좀 특이한 분야입니다. 하지만 제 생각에는 근본적인 질문은 '사물이 어떻게 동일한가?', 즉 '이러한 것들의 기본 구조는 무엇인가?'입니다. 따라서 Haskell에서 본 그 질문을 통합하고 싶었습니다. Haskell은… 음… 타입 클래스와 여러 타입에 걸친 균일한 동작… 그리고 모든 것… 음… 음… 그래서 그 분야에서 더 발전된 것을 찾게 되었고… 음… 결국… 음… 디팬던트 타입을 접하게 되었습니다. 그리고 석사 과정은 Agda가 개발된 샬머스에서였기 때문에… 음… 네, Haskell에서 범주론, 디팬던트 타입으로… 음… 복잡 시스템과 결합하게 되었습니다. 음… 그리고 Agda는 자연스러운 선택이었습니다. 그리고… 음… 샬머스… 좋아요. 감사합니다. 다른 질문 있으신가요? 없으시다면… Andrea에게 다시 한번 감사드립니다. 네, 감사합니다.

](https://www.youtube.com/watch?v=OSDgVxdP20g

네, 알겠습니다. 모든 내용을 요약하지 않고 한글로 번역해 드리겠습니다.

예, 라이브 방송입니다. 안녕하세요 여러분, 따뜻하게 FunR에 오신 것을 환영합니다.

이번에는 스웨덴입니다. 올해 두 번째 방문이네요. 우리는 지금 스톡홀름에 있는 KRA 사무실에 있습니다. 정말 멋진 사무실이네요. 저희를 이 멋진 스톡홀름 사무실에 초대해 주셔서 KRA에 진심으로 감사드립니다.

정말 감사합니다. 바로 시작하겠습니다. 먼저 저 Magnus가 짧게 소개를 하고, 그다음 Andrea가 Super Husc, Agda 소개를 할 것입니다. 그 후에는 Lash가 Scala를 이용한 스키마 관리에 대해 발표할 것입니다.

재밌는 사실은 Lash는 원래 3년 반 전에 이 발표를 하기로 되어 있었는데 코로나가 발생하면서 3년 반이 지난 지금, 드디어 여기서 발표를 하게 되었습니다. 정말 기쁩니다.

네, 정말 기쁩니다. 마지막에는 제가 다시 한번 Meetup을 요약할 것입니다. 저희를 이곳에 초대해 주셔서 KRA에 다시 한번 감사드립니다. KRA 직원들과 이야기하고 싶으시면 초록색 옷을 입은 사람들을 찾으세요.

초록색, 네. 또한 비디오 스트림을 후원해 주신 Other The Beat에도 감사드립니다. Other The Beat에 대해 더 알고 싶으시면 인터넷을 참고하세요.

그리고 올해 남은 일정은 11월 7일에 또 다른 Meetup으로 돌아오고 12월 5일에도 Meetup이 있습니다. 1월에는 아직 날짜를 정하지 않았지만 물론 Meetup이 있을 것입니다.

FunR Sweden Meetup을 지원하고 싶으시면 Meetup으로 이동하여 Meetup 커뮤니티에 가입하세요. 매우 간단합니다.

그리고 물론 YouTube로 이동하여 구독, 좋아요 등 YouTube에서 할 수 있는 모든 것을 하세요. Google이 여러분을 좋아할 것이고, 저희도 여러분을 좋아할 것입니다.

그리고 저희는 Discord 채널도 개설했습니다. YouTube 채팅에서 긴 질문을 하기 어려울 때가 있습니다. Discord에 참여하시면 발표자에게 길고 까다로운 질문을 할 수 있습니다.

그래서 발표 중에 질문이 있으시면 채팅이나 Discord 채널에 올려주시거나, 여기에 계시다면 손을 들어주세요. 질문이 있으신가요?

네, 그럼 시작하겠습니다. 첫 번째 발표는 Andrea의 Super Husc, Agda 소개입니다.

환영합니다, Andrea. 노트북을 넘겨드리겠습니다. 감사합니다, Magnus.

네, 감사합니다.

좋아요, 마이크가 작동하는군요. 여기서 확인해 보죠.

시작하겠습니다. 참석해 주시고 제 강연을 들어주셔서 감사합니다. 잠시 제 폰으로 설정을 좀 하겠습니다.

이제 시작해 볼까요? 제가 Super Haskell이라고 부르는 언어를 탐험해 보겠습니다.

먼저 저를 간단히 소개하겠습니다. 저는 브라질 출신의 소프트웨어 엔지니어이지만 스웨덴에 약 3년 동안 살고 있습니다. Adatabt에서 FP 컨설턴트로 일하고 있으며, 요즘에는 Purescript를 사용하고 있습니다. 예테보리 대학교에서 석사 학위를 받았고, 범주론과 동적 시스템을 Agda로 연구했습니다. 물론 저는 Agda 전문가는 아닙니다.

그 점을 미리 말씀드리고 싶지만, 여러분의 흥미를 끌 만큼은 충분히 알고 있다고 생각합니다. 이 강연은 제 생각에는 아주 대략적인 추정이지만 TI가 많은 부분을 차지할 것 같습니다. Agda 언어와 그 기반 이론에 대한 철학과 동기 부여를 조금 다루고, Agda의 핵심 개념을 소개하는 코드 예제를 살펴본 후 Agda를 사용하여 매우 작지만 실제적인 프로그램을 실행해 보겠습니다.

**우선 왜 디팬던트 타입을 사용해야 할까요? 왜 디팬던트 타입을 사용하는 프로그래밍을 해야 할까요? 제가 생각하기에 코드를 작성할 때, 소프트웨어 엔지니어링을 할 때, 우리는 일반적으로 코드가 정확한지 여부에 신경 씁니다. 저는 이것을 두 가지 유형의 작업으로 봅니다. 하나는 코드를 구현하는 것입니다. 즉, 함수의 본문을 작성하는 것이죠. 하지만 또 다른 하나는 방금 작성한 코드에 대해 생각하고 정확성을 보장하며 실제로 원하는 대로 작동하는지 검증하는 것입니다. 이 그래프에서 '정확성 보장'과 '구현'이라는 용어는 매우 중복되어 있습니다. 프로그램을 정확하게 디버깅하는 데 필요한 신뢰도는 다양합니다. 즉, 상황에 따라 다른 기준을 가지게 되고 구현에 필요한 작업량도 달라집니다. 어떤 사람들은 Python으로 코드를 작성하는 것이 매우 쉽다고 생각할 것이고, 어떤 사람들은 Haskell이나 Agda, 또는 다른 언어로 코드를 작성하는 것이 쉽다고 생각할 것입니다. 저는 우리가 적절한 균형을 찾아야 한다고 생각합니다. 저는 조금 긴장되네요.

예를 들어, 소셜 미디어 웹사이트가 평소보다 느린 것보다 원자력 발전소 소프트웨어에 오류가 있는 것이 훨씬 더 심각합니다. 그리고 우리는 정확성을 보장하기 위해 몇 가지 도구를 사용할 수 있습니다. 테스트가 있지만, 분명히 완벽하지는 않습니다. 프로그램이 정확한지 확인하기 위해 가능한 모든 테스트를 생각해 낼 수는 없을 것입니다. 신뢰도 있습니다. 이것은 오랫동안 사용되어 왔고 오랫동안 잘 작동해 왔기 때문에 앞으로도 계속 작동할 가능성이 매우 높다는 것입니다. 이것은 린디 효과로 알려져 있습니다. 무언가가 영원히 존재해 왔다면 영원히 존재할 것입니다. 하지만 항상 그런 것은 아닙니다. 여기 계신 많은 분들이 Log4j 문제를 기억하실 것입니다. 아주 오래된 Java 라이브러리에 취약점이 있었는데, 제 생각에는 몇 년 전에 발견된 것 같습니다. 그리고 타입과 정리도 그것들이 실제로 말하는 대로 작동한다는 보장은 아닙니다. 즉, 신뢰도가 보장되지 않는다는 것입니다.

컴파일러에도 버그가 존재합니다. GHC 9.4.1에는 부동 소수점 오류가 있었고, 증명 검사기에는 불일치가 존재합니다. Agda의 확장 기능인 Cubical Agda의 개발 버전에서 불일치가 발견되었습니다. 이는 기본적으로 해당 버그를 악용하면 무엇이든 증명할 수 있다는 것을 의미합니다. 따라서 우리는 절대 확신할 수 없습니다.

물론 우리는 신뢰도를 높일 수 있습니다. Agda와 디팬던트 타입이 제공하려는 도구는 인간의 의도와 기계 코드 사이의 간극을 좁히는 것입니다. 즉, 전자가 전선에서 우리가 원하는 방식으로 움직이도록 하는 것입니다. '내가 의도한 바가 아니었어'라고 말하는 횟수를 줄이고 싶습니다. 그리고 이 맥락에서 타입에 대해 생각해 보면, 올바른 모양을 올바른 구멍에 넣어야 하는 어린이 장난감이 떠오릅니다. 제 생각에는 프로그래밍의 많은 부분이 이런 연결 작업으로 귀결됩니다. 여기서 비유하자면, 구멍의 모양은 함수를 호출할 때 넣어야 하는 것의 타입입니다. 그리고 구멍을 만드는 표면은 타입 시스템과 같습니다. 즉, 타입 시스템을 통해 특정 모양을 표현할 수 있습니다. 이제 올바른 모양을 올바른 구멍에 넣는다는 것이 무엇을 의미하는지 생각해 보겠습니다. 이 경우에는 H1 모양을 H1 구멍에 넣고 싶을 것입니다. 여기에 라벨을 붙이지는 않았지만 1, 2, 3이고 정사각형을 정사각형에, 원을 원에 넣고 싶을 것입니다. 이것을 보면 선택의 여지가 거의 없습니다. 물론 원을 정사각형 안에 넣을 수도 있지만, 그렇게 하려면 상당한 노력이 필요할 것입니다. 실제로는 모양을 가져다가 넣기만 하면 됩니다. 이것이 바로 이것이 전달하려는 내용입니다. 반면에 타입이 없는 언어에서는 모든 것이 정사각형과 같습니다. 이제는 정말 선택의 여지가 없습니다. 라벨을 읽고 '오른쪽에 있는 이것은 왼쪽 구멍에 들어가야 하는 것이고, 이것은 여기로 가고 저것은 저기로 가야 하는구나'라고 말해야 합니다. 즉, 더 많은 인지적 노력이 필요합니다. 제 생각에 Agda가 해당되는 Super Type 언어에서는 이러한 구멍의 모양을 매우 구체적으로 만들 수 있습니다. 즉, 타입 시스템을 통해 거의 모든 것을 표현할 수 있습니다. 그 안에 들어맞는 것은 단 하나뿐입니다.

하지만 비유를 계속 이어가자면, 이러한 구멍을 깎아내야 하는 표면에서 작업하고 있고 표면이 너무 약해서 작은 구멍을 만들거나 여기 조금 깎아내면 전체가 부서지고 저기에 작은 균열이 생길 수 있습니다. 이것은 우리가 원하는 것이 아닙니다. 반면에 너무 탄력적이면 이러한 구멍 중 하나를 가져다가 있는 힘껏 무언가를 밀어 넣으면 반대쪽으로 나오고 어떻게든 작동할 것입니다. 마치 TypeScript 코드에 any를 넣는 것과 같습니다. 따라서 우리는 적절한 재료를 원합니다. 제 생각에는 편의성과 정확성 사이에 적절한 균형점이 있습니다. 그리고 적절한 재료를 갖추지 못하는 경우는 두 가지 방향에서 발생할 수 있습니다. 하나는 타이핑 비용이 너무 높을 때입니다. 이 소식을 보셨는지 모르겠지만 최근에 Svelte가 TypeScript를 포기했습니다. 저는 그에 대해 잘 알지 못하지만, 실제로 이런 일이 일어날 것이라고는 예상하지 못했습니다. 지금까지는 일반적으로 모든 사람들이 모든 것에 타입을 계속 추가할 것이라고 생각했습니다. 왜냐하면 편의성의 비용이 높을 수 있기 때문입니다. 그래서 프로토타입을 만들기 쉽고 편리한 동적 타입 언어가 계속해서 타입 시스템을 추가하는 것입니다. 그리고 적절한 재료를 얻는 것은 어렵습니다. 이것은 제가 작업하고 있는 Purescript 라이브러리의 코드 조각입니다. 읽을 수 있는지 모르겠지만, 중요하지 않습니다. 요점은 이것이 코드의 벽이라는 것입니다. 그리고 이것은 그렇게 복잡하지 않은 것을 표현하고 있습니다.

그리고 여기에 타입에 대해 많이 알고 있는 정말 뛰어난 프로그래머인 Conor McBride의 답변이 있습니다. 그는 Haskell에 Singletons 라이브러리에 대해 말했습니다. 들어보셨는지 모르겠지만 기본적으로 Haskell에 디팬던트 타입을 모방하여 Haskell이 이미 가지고 있는 것보다 더 많은 타입 안전성을 추가하는 것입니다. 여기서 질문은 Singletons를 사용하면 무엇을 얻을 수 있는가였습니다. 그리고 그의 답변은 '그것은 우리가 다시는 보지 않기를 바라는 성가신 것입니다'였습니다. 하지만 저는 Agda가 이 균형을 맞추는 데 매우 근접했다고 생각합니다. 그리고 여기에 언어를 소개하는 슬라이드가 하나 더 있습니다.

Agda는 샬머스에서 개발된 디팬던트 타입의 순수 함수형 언어입니다. 문법은 Haskell과 매우 유사하지만 몇 가지 중요한 차이점이 있습니다. 곧 살펴보겠습니다. Hindley-Milner 대신 Martin-Löf 타입 이론을 기반으로 합니다. 왼쪽에 있는 분이 스웨덴 논리학자인 Martin-Löf입니다. 재밌는 사실은 Agda라는 이름이 Cornelis Vreeswijk의 노래에서 따왔다는 것입니다. 이것이 바로 그 아이콘입니다. 저는 이것이 닭이라는 것을 알아차리는 데 시간이 좀 걸렸습니다. 스웨덴 사람인 Ulf Norell이 만들었습니다.

옆에 있는 작은 표는 기본적으로 Agda가 어떻게 타입과 값의 구분을 모호하게 하려고 하는지 보여줍니다. Agda는 단순히 꽤 균일한 방식으로 사물을 던지지만, 일부 고급 언어에서는 각각이 고유한 구문적 요소로 취급됩니다. 실제로 동일한 것을 표현하는 방식이 다릅니다.

하지만 철학과 동기 부여에 대한 이야기는 이 정도로 마무리하겠습니다. 이제 Agda 코드를 보고 싶어 하실 거라고 생각합니다. 이것이 바로 제가 이러한 슬라이드를 통해 의도한 바입니다. 그럼 시작해 볼까요? 여기에 준비해 둔 몇 가지 모듈이 있습니다. 하나는 언어의 문법을 설명하는 것입니다. 타입, 함수 등을 정의하는 방법을 보여드리겠습니다. 그런 다음 타입으로서의 명제라는 개념에 대해 알아보겠습니다. 이 방에 계신 분들 중에 타입으로서의 명제가 무엇을 의미하는지 아시는 분이 계신가요? 아시는 분은 손을 들어주세요. 몇 분 계시네요. 좋습니다. 제가 여러분의 언어로 말하고 있는지 확인하고 싶었습니다. 그런 다음 몇 가지 기본적인 행렬 연산을 포함하는 매우 작은 행렬 라이브러리를 살펴보고 마지막으로 Agda의 탈출구 역할을 하는 Haskell FFI에 대해 알아보겠습니다. 그럼 시작해 보죠. 이것은 문법을 소개하는 첫 번째 모듈이고 몇 가지… 잠시 제 폰 도우미를 업데이트하겠습니다. Agda 모드에 대해 몇 가지 말씀드리겠습니다. 제 생각에 대부분의 Agda 프로그래머는 Emacs를 사용하는 것 같습니다. 저는 Emacs를 사용해 본 적이 없지만, 'Control-C Control-어쩌구'와 같은 명령이 많다고 합니다. 그리고 이것은 그냥... 무언가를 요청하는 명령입니다. 예, 감사합니다. 불을 좀 밝혀주시겠어요? 너무 어둡다는 의견이 있네요. 사실 저는 VS Code에서 그걸 어떻게 바꾸는지 모르겠습니다. '선호하는 밝은 색상'은 없습니다. 누군가 뭔가를 제안했는데... 'Command-K Command-T'인가요? 아, 좋습니다. 훨씬 보기 좋네요. 감사합니다. 글꼴 크기도 좀 키울 수 있을 것 같습니다. 마지막까지는 보이지 않겠지만요. 좋아요, 더 보기 좋나요? 좋습니다.

네, Agda 모드는 코드를 작성할 때 도움을 주는 여러 가지 명령어입니다. 이것들이 주요 명령어이고 저는... 바로 그 Conor McBride가 키보드 위에 카메라를 설치해서 어떤 명령어를 실행하는지 보여주는 기술을 사용할 것입니다. 여기에도 표시됩니다. 잘 보시면 제가 이러한 명령어를 실행할 때 확인하실 수 있을 것입니다. 하지만 네, 단일 모듈을 로드하고 타입 검사를 하고, 전체를 개선하는... Agda 프로그래밍과 테스트, REPL 작업의 99%가 여기서 이루어집니다. REPL과 동일한 환경입니다. 그리고 출력은 모두 이 작은 탭에 표시됩니다. 그럼 시작해 보죠. 먼저 몇 가지 타입과 값이 있습니다. 이것은 Haskell의 GADT 문법과 매우 유사합니다. 익숙하신 분들은 'data'라고 하면... 이것은 타입의 이름이고 저것은 타입의 타입입니다. 네, Agda에는 'kind'가 없습니다. 타입은 그냥 타입을 가집니다. '집합'이라고 불립니다. 왜냐하면 타입은 실제로 값의 모음일 뿐이기 때문입니다. 여기서 이 생성자는 3에서 3으로 가는 타입을 가지고 있습니다. 등등. 그리고 이것은 타입 3의 값의 예입니다. 그리고 또 다른 하나. Agda는 보시다시피 유니코드를 지원합니다. 이 작은 2… Agda는 유니코드를 매우 적극적으로 사용합니다. 매우 흔한 일이며 우리는 유니코드를 많이 사용할 것입니다. 하지만 이것은 타입 3의 두 가지 다른 값입니다. 이것이 합 타입을 정의하는 방법입니다. 여기에 Haskell의 'Either'와 동일한 것이 있습니다. 보시다시피, Haskell이나 Purescript, 또는 다른 방언을 보신 적이 있다면 이것은 매우 유사해 보입니다. 왼쪽에 타입이 있고 오른쪽에 타입이 있으며 'Either a' 또는 'b'를 얻는 방법은 두 가지입니다. 'Left' 주입을 수행하여 타입 'a'의 요소를 가져와서 타입 'Either a' 또는 'b'의 요소를 반환하거나, 오른쪽에서 수행할 수 있습니다. 그리고 여기에 'Either'의 값이 있습니다. 여기서 우리는 또 다른 문법 요소를 도입했습니다. 이것은 암시적 매개변수입니다. 따라서 이 값을 호출할 때, 이 값을 사용할 때, 우리는 일반적으로 타입 'a'가 무엇인지 말하고 싶지 않습니다. 문맥에서 분명할 것입니다. 하지만 실제로는 꽤 자주 이 인수를 제공해야 합니다. 따라서 이것은 'value of either'가 자연수 또는 모든 타입의 'Either' 타입을 가진다는 것을 말하고 있습니다. 왜냐하면 'Left 10'이기 때문입니다. 자연수...

그리고 여기에 곱 타입의 문법이 있습니다. 'record'라는 다른 키워드가 사용된 것을 알 수 있습니다. 그리고… 네, 그 이유는 곱 타입과 합 타입 사이에 근본적인 차이점이 있기 때문입니다. 서로 이중 관계입니다. 그리고 개인적으로는 레코드의 필드가 무엇인지, 곱 타입이 무엇인지 지정하는 작은 섹션이 있는 것이 보기 좋다고 생각합니다. 혹시 모르시는 분들을 위해 말씀드리자면, 두 가지는 동일합니다. 좋아하는 프로그래밍 언어로 레코드를 정의할 때마다 실제로는 곱 타입을 정의하는 것입니다. Agda는 이를 매우 명확하게 보여줍니다. 그리고 이러한 타입 중 하나를 빌드하기 위해 생성자를 제공할 수 있습니다. 여기서 사용되는 것을 볼 수 있습니다. 따라서 이것은 3의 값 하나와… 6이라는 타입과 6의 값을 포함하는 쌍입니다. 생성자를 사용하여 빌드하기만 하면 됩니다.

여기에 Haskell의 튜플 타입 정의가 있습니다. 두 가지 다른 타입의 쌍입니다. 다시 말하지만, 두 가지 타입을 매개변수로 사용합니다. 하나는 첫 번째 필드에, 다른 하나는 두 번째 필드에 들어갑니다. 매우 간단합니다. 이것이 쌍을 구성하는 방법입니다. 쌍 생성자에 이름을 지정했기 때문에 Haskell과 달리 생성자를 대문자로 쓸 필요가 없는 것을 알 수 있습니다. 네, 매우 기본적인 내용입니다. 여기에 함수를 정의하는 방법의 예가 있습니다. 다시 말하지만 Haskell과 유사합니다. 두 자연수를 가져와서 더하는 함수와 인수 중 하나에 대해 패턴 매칭을 수행하는 함수가 있습니다. 따라서 3개 값 중 하나를 자연수에 더합니다. 따라서 값이 1이면 1을 더하고, 2이면 2를 더합니다. 등등. 그리고 이것은 여전히... Haskell과 매우 유사해 보입니다. 그렇죠? 그리고 꽤 멋진 몇 가지 문법적 요소를 더 살펴보겠습니다. Agda는 중위 연산자를 지원합니다. 따라서 이 함수의 이름은 꽤 이상하지만, 사용할 때는 의미가 있습니다. '첫 번째 인수를 두 번째 인수에 더하되, 무언가와 무언가가 참이면 그렇게 하고 그렇지 않으면 둘 중 하나를 선택합니다.' 따라서 4개의 인수를 사용합니다. 4개의 작은 밑줄입니다. 그리고 자연수를 반환합니다. 여기서 본문을 볼 수 있습니다.

let 바인딩은 Haskell과 동일하게 작동합니다. 따라서 '조건 1'과 '조건 2'를 수행합니다. 여기서는 부울 연산자입니다. 그리고 둘 다 참이면 합하고 그렇지 않으면 둘 중 하나를 선택합니다. 어떻게 선택할까요? where 블록에 정의된 이 함수를 사용합니다. 그리고 이 함수는 Agda에서 case와 같은 역할을 하는 with 키워드를 사용합니다. 그리고 이것은 실제로 의존 패턴 매칭입니다. 즉, with 내부의 표현식에 대해 패턴 매칭을 수행할 때 컴파일러는 패턴 매칭 본문에 있는 타입에 대해 알고 있습니다. 제 생각에는 with를 사용하는 예를 볼 수 있을 것 같습니다. 대부분의 경우에는 필요하지 않을 것 같습니다. 그리고 이 경우에는 이것은 의존적이지 않은 패턴 매칭입니다. 거짓이면 'm'을 반환하고 그렇지 않으면 'n'을 반환합니다. 하지만 네, 이렇게 생겼습니다. 자, 여기 값이 있습니다. 15를... 10을 5에 더하지만 true이고 5가 10보다 작을 때만 그렇게 하고 그렇지 않으면 둘 중 하나를 선택합니다. 이것은 15입니다. 그리고 여기에 숫자를 가져와서 15를 더하는 'add 15'가 있습니다. 이것은 람다 문법을 보여주기 위한 것입니다. 람다는 이렇게 멋진… 유니코드 람다입니다. 실제 그리스 문자와 같습니다. 보기 좋다고 생각합니다. 따라서 Haskell에서 이것은… 이 함수가 '자연수에서 자연수로' 가는 타입을 가지고 있다고 말하고 있습니다. 그리고 이 값은 '자연수에서 자연수로' 가는 타입의 무언가입니다. 이 값은 무엇일까요? 자연수를 가져오는 함수입니다. Haskell에서처럼 이렇게 쓸 수도 있었을 것입니다. 네, 람다가 있습니다.

이제 타입으로서의 명제에 대해 알아보겠습니다. 왜냐하면 유용한 디팬던트 타입 프로그래밍을 하려면 이것을 이해해야 하기 때문입니다. 따라서 문법 모듈을 가져오겠습니다. import 이름 앞에 'open'이 있는 것을 보셨을 것입니다. 이것은 이 모듈의 모든 것을 범위로 가져와서 최상위 변수처럼 취급하라는 의미입니다. 여기… 모듈에서 항목을 숨길 수 있습니다. 따라서 여기서는 몇 가지 항목을 가져오고 있습니다. 최소한으로 유지하려고 노력했습니다. 표준 라이브러리에서 가져오는 항목은 이 정도입니다. 하지만 항목을 숨길 수 있습니다. 이름을 숨길 수 있습니다. 그리고 이제 실제로 디팬던트 타입에 대해 알아보겠습니다. 따라서 여기 이 타입은 동등 타입입니다. 그리고 이것은… 모든 타입… 집합에 대해… 그리고 'x'가 멤버인... 집합의 멤버인 모든 타입에 대해… 그리고 해당 타입의 모든 요소에 대해 이 타입의 요소를 제공하면 집합을 반환합니다. 좋아요.

그리고 이 타입의 유일한 구성원인 'refl'은… 'x'는 'x'와 같다는 타입을 가지고 있습니다. 따라서 이것은… 이 타입에 대해 패턴 매칭을 수행할 수 있는 유일한 방법, 이 타입으로 무언가를 할 수 있는 유일한 방법은 동일한 두 값이 있는 경우뿐이라는 것을 의미합니다. 좋아요. 따라서 여기 'x'는 이 생성자의 양쪽에 있습니다. 보이시나요? 여기에도 나타나고 여기에도 나타납니다. 콜론의 왼쪽에 나타나는 타입과 오른쪽에 나타나는 타입 사이에는 차이가 있습니다. 하지만 저는 그 부분에 대해서는 자세히 설명하지 않겠습니다. 제가 보여드리고 싶은 것은… 이것이 두 개의 매개변수를 사용하더라도 실제로 동일한 경우에만 값을 구성할 수 있다는 것입니다. 좋아요.

따라서 Agda는 타입 수준에서 이를 계산할 수 있습니다. 여기에 구멍이 있습니다. 이 모듈에서 'Control-C Control-L' 명령어를 실행한 첫 번째 결과입니다. 이것은 'hole0'이고 이 구멍은… '11 + 4'는 '15'와 같다는 타입을 가지고 있습니다. 이전에 정의한 값입니다. 이것의 타입입니다. 따라서 이것이 타입으로서의 명제가 '11 + 4는 15와 같다'는 명제를 표현하는 방법입니다. 타입… 제가 이것을 말하지 않은 이유는 다시 똑같은 말을 반복해야 하기 때문입니다. 하지만 둘은 동일합니다. 명제는 타입입니다. 그냥 그렇습니다. 이것은 논리학과 컴퓨터 과학의 기본적인 사실입니다. 따라서 이 타입의 구성원은 무엇일까요? 타입… 네, 이 두 값에 대한 '동등' 타입의 고유한 구성원입니다. 그리고 이제 저는 Agda가 이를 자동으로 해결하도록 매우 강력한 명령어인 'Control-C Control-A'를 사용하겠습니다. Agda는 이 명제의 증명이 이 타입의 값이라는 것을 알아낼 수 있습니다.

이것이 바로 대응 관계입니다. 명제는 타입이고 증명은 값 또는 프로그램입니다. 타입의 값은 해당 타입이 참이라는 증거입니다. 곧 이에 대한 몇 가지 예를 더 살펴보겠습니다. '1 + 13'이 '15'와 같다는 것을 증명하고 싶다면… 그것은 불가능합니다. 이 점에 대해서는 여러분을 굳이 설득할 필요가 없을 것 같습니다. 하지만 제가… 이제 여기서 문맥을 보여주는 명령어를 사용하겠습니다. 제가 보여드리려는 것은… 이것이 우리가 보는 출력입니다. 컴퓨터 숫자 14가 컴퓨터 숫자… 15와 같다는 것을 보여드리려고 합니다. 실제로는 보여줄 수 없습니다. 곧 문맥을 사용하는 몇 가지 예를 더 살펴보겠습니다. 충분합니다. 따라서 타입으로 다른 관계를 정의할 수 있습니다. 예를 들어 숫자가 다른 숫자보다 작거나 같다는 것, 또는 실제로 무엇이든… 네, 모든 명제… 하지만 이를 생각하는 또 다른 방법이 있습니다. 타입이 참이면 구성원이 있습니다. 적어도 하나의 값이 있습니다. 적어도 하나의 요소가 있는 집합입니다. 구성원이 없으면 아무것도 없습니다.

그리고 이 두 가지 기본적인 참 또는 거짓 상태는 이 두 가지 타입으로 표현됩니다. 하나는 ⊥(bottom)이라고 하고 다른 하나는 ⊤(top)이라고 합니다. 좋아요. 무서운 소리네요. 화재 경보인가요? 좋아요. 이제 훨씬 덜 무섭네요. 네, 따라서 이 두 가지 타입은 각각 구성원이 없고 하나의 요소로 구성됩니다. 하지만 ⊥는 분명한 이유로 거짓이라고도 합니다. 근본적으로 거짓인 명제를 나타냅니다. 그리고 ⊤는 참이라고 합니다. ⊤는 'tt'라는 단일 구성원을 가지고 있으며, 이 값은 ⊤ 타입으로 표현되는 명제가 참이라는 증거입니다. 따라서 이제 의존 함수를 사용하여 이러한 타입을 기반으로 관계를 정의할 수 있습니다. 이것을 보세요. 이것은 두 자연수를 가져와서 집합을 반환하는 함수입니다. 타입을 반환합니다. 좋아요. 그리고 이것의 논리를 생각해 보겠습니다. 0이 'n'보다 작거나 같으면… 첫 번째 인수에 대해 패턴 매칭을 수행하면 참이라는 것을 알 수 있습니다. 0은 다른 모든 자연수보다 작거나 같습니다. 따라서 ⊤ 타입으로 표현합니다. 그리고… 네, 이것은 구멍이었어야 했는데... 이제 다른 구멍을 채워보겠습니다. 이 경우는 어떨까요? 숫자의 후속자가 있는 경우… 피아노… 이걸 물어봤어야 했는데… 자연수의 피아노 표현은 0은 자연수이고 자연수의 후속자는 자연수라는 것입니다. 이것은 귀납적 정의이며 여기서 패턴 매칭을 수행하는 것입니다. 따라서 자연수의 후속자… 자연수가 될 수 있는 가장 작은 수는 0이므로 왼쪽의 것은 적어도 1이고 1 또는 1보다 큰 수는 0보다 작거나 같지 않습니다. 따라서 이것은 ⊥ 타입입니다. 이것이 바로 우리가 표현하려는 것입니다. 이것이 우리가 정의하는 관계입니다. 그리고 타입...

그리고 두 자연수가 모두 무언가의 후속자인 경우는 어떨까요? 네, 왼쪽의 것이 오른쪽보다 작거나 같으려면 둘의 전임자가 오른쪽보다 작거나 같아야 합니다. 따라서 이것은… 모니터가 느리네요. 이것은… 이렇게 됩니다. 관계를 재귀적으로 호출하고 있습니다. 그리고 여기서 이것이 작동한다는 작은 증명을 할 수 있습니다. 네, 0이… 100보다 작거나 같다는 것을 예상해야 합니다. 그리고 우리의 목표가 무엇인지, 이것이 참이라는 증거를 제공하기 위해 무엇을 제공해야 하는지 알 수 있습니다. ⊤ 타입입니다. ⊤ 타입에는 단 하나의 구성원이 있습니다. Agda에게 타입의 값을 제공하도록 요청할 수 있는지 궁금하네요. ⊤ 타입… 물론 가능합니다. 구성원이 하나뿐이기 때문에 Agda는 타입을 보고 이것이 참이라는 것을 알 수 있습니다. 또는… 무엇을… 무엇을… 타입을 계산한 다음 '좋아요, 이것이 제공해야 하는 것입니다. 이것이 제공해야 하는 증거입니다'라고 말합니다. 그리고 증거는 사소합니다.

우리는 엄격한 부등식도 가지고 있습니다. 따라서 여기서 우리는 0이 0보다 작지 않다는 것을 말하고 싶습니다. 이번에는… 여기에 ⊥가 있습니다. 이것도 분명히 거짓입니다. 다른 모든 것보다 크거나 같은 것은 분명히 0보다 작지 않습니다. 하지만 0은 모든 후속자보다 작거나 같습니다. 따라서 이것은 ⊤가 될 것입니다. 그리고… 마지막 경우에 대한 재귀 호출입니다. 또한 저에게는 치트 시트가 있습니다. 아시다시피 라이브 코딩은 어렵습니다. 그리고 사실 생각보다 진행 속도가 느려서… 타입으로서의 명제 모듈의 후반부는 구멍을 해제하고 코드를 살펴보는 방식으로 빠르게 진행하겠습니다. 왜냐하면 시간이 부족하기 때문입니다. 다룰 내용이 꽤 많습니다. 따라서 이것은 무엇을 말하는 것일까요? 타입… 타입 안전 뺄셈… 'm'보다 작은 'n'은… 'n'이… 'm'보다 작다는 증거를 제공하는 경우에만 또 다른 자연수를 제공합니다. 그리고 여기에 Agda가 하는 일이 있습니다. 오른쪽에 0이 있으면 이미… 왼쪽의 것이 오른쪽보다 크거나 같다는 것을 이미 알고 있기 때문에 'tt' 값을 제공할 수 있습니다. 미리 계산했습니다. 따라서 'm'에서 0을 뺀 것은… 분명히 'm'입니다. 이제 'm'에서 무언가의 후속자를 뺀 경우… 이것은 무엇이 되어야 할까요? 네, 이것이 참이라는 증거를 제공할 수 없습니다. 이 방정식의 이 부분에 대한 증거를 제공할 수 없습니다. 그리고 이것에 대한 증거가 있다면 ⊥ 타입의 구성원을 갖게 될 것이고, 그것은 존재하지 않습니다. 따라서 이를 표현하는 방법은 여기 이 빈 괄호입니다. Haskell이나 그와 같은 것의 unit이 아닙니다. 그리고 무언가의 후속자에서 무언가의 후속자를 빼고 왼쪽이 오른쪽보다 크다는 증거가 있다면… 재귀적으로 뺄셈 함수를 호출하여… 이 숫자의 전임자를 제거합니다. 따라서 여기서 우리의 뺄셈이 정확한지 테스트할 수 있습니다. 뺄셈 함수... 그리고 예상하셨겠지만, Agda는 이를 자동으로 계산할 것입니다. 타입을 보고 방정식의 양쪽이… 동일하다는 것을 알 수 있습니다. 그리고 이것이 기본적으로 타입으로서의 명제의 개념입니다. 더 고급 증명을 할 수도 있지만, 저는 디팬던트 타입으로 프로그래밍하는 부분을 다루고 싶습니다. 따라서 여기서 조금 조금 더 빠르게 진행하겠습니다. 이것은 디팬던트 타입의 전형적인 예입니다. 컴파일 타임에 벡터의 길이를 알 수 있는 벡터입니다. 물론 미리 알 수 있다는 의미는 아닙니다. 사용자 입력 등을 받을 수 있지만, 요점은 타입의 일부라는 것입니다. Haskell이나 다른 언어의 벡터... 네, 대부분의 언어에서는 일반적으로 벡터는 다른 타입을 포함할 뿐입니다. 타입 자체에 길이가 연결되어 있지 않습니다. 하지만 이 경우에는 'Vec'입니다. 이 타입은 어떻게 정의될까요? 길이가 0인 'Nil' 벡터가 있고 'Cons' 벡터가 있습니다. 이 생성자는 요소를 가져오고 다른 벡터를 가져와서 해당 타입의 요소가 그만큼 있는 벡터를 반환합니다. 더하기 1. 받은 첫 번째 요소를 앞에 붙이기만 하면 됩니다. 그리고 여기에… 이제 줄 바꿈이… 단어 줄 바꿈을 전환할 수 있습니다. 네, 그렇게 하면 아무것도 놓치지 않을 것입니다. 여기에 'take' 함수가 있습니다. 저는… 이것을 채우는 대신 치트 시트를 사용하겠습니다. 이런… 'take' 함수는… 숫자를 제공하고 벡터를 제공하면 앞에서부터 해당 개수만큼 요소를 가져온 벡터를 반환합니다. 하지만 이 경우에는 제공하는 숫자가 벡터의 길이보다 작다는 증명을 제공해야 합니다. 숫자 'a'를 제공하고 'a'가 길이보다 작다는 증명을 제공하면 첫 번째 벡터에서 가져온 길이 'a'의 벡터를 제공합니다. Haskell에서 이것을 본 적이 있을 수도 있습니다. 여기에는 특별한 것이 없습니다. 0을 가져오면 빈 벡터를 반환합니다. 무언가의 후속자를 가져오면… 요소를 하나 가져와서 벡터의 뒤로 이동합니다. 여기에 두 벡터를 연결하는 것이 있습니다. 치트 시트를 사용하겠습니다. 빈 벡터가 있으면 실제로는 빈 벡터를 두 번째 벡터와 연결하는 것이므로 두 번째 벡터를 반환하기만 하면 됩니다. 반면에 첫 번째 벡터에 무언가가 있으면 그것을 순회하고 나머지를 연결한 결과 앞에 놓습니다. 여기에 벡터에서 요소를 가져오는 것이 있습니다. 다시 말하지만 벡터의 길이가 있고… 아… 'wp'라는 단어는 좀 안 좋은 생각이었던 것 같지만, 여기서 아이디어를 얻을 수 있습니다. 찾고 있는 인덱스가 길이보다 작다는 증명이 있습니다. 해당 요소의 무언가를 얻을 수 있습니다. 'take'와 매우 유사한 아이디어입니다. 싱글톤을 구성합니다. 싱글톤을 잘 활용하고 있습니다. 중위 연산자... 여기에 요소를 제공하면 해당 요소가 있는 길이 1의 벡터를 반환합니다. 여기에 우리의… 오른쪽 인덱스가 작동한다는 작은 증명이 있습니다. 자동 해결… 아기… Agda는 알고 있습니다. 'v' 벡터에서 인덱스 2를 찾는다는 타입을 지정합니다. 여기서 바인딩한 'v'입니다. 네, 타입에 let 바인딩이 있는데, 제 생각에는 정말 멋진 기능입니다. 그것은 6과 같습니다. 네, 물론입니다. 그리고 몇 가지 일반적인 고차 함수... 네, 'map'... 'map'을 좋아하지 않는 사람이 있을까요? 함수를 벡터에 적용하고 벡터의 나머지 부분을 순회하면서 함수를 적용합니다. 여기에 지점별 적용이 있습니다. 함수가 있고 길이가 'n'인 벡터가 있습니다. 이 벡터는 'a'에서 'b'로 가는 함수를 포함합니다. 그리고 'a'의 벡터를 제공하면 'b'의 벡터를 얻을 것으로 예상합니다. 이것은… 매우 일반적인 고차 함수는 아닙니다. 적용 가능한 펑터를 떠올리게 할 것입니다. 하지만 곧 사용할 것이기 때문에 여기에 포함했습니다. 또한 'replicate'를 사용할 것입니다. 'replicate'는 요소를 제공하면 길이가 'n'인 벡터를 제공합니다. 'n'이 무엇이든... 'n'은 여기서 암시적 인수로 제공됩니다. 하지만… 'n'이 0일 때… 다시 말하지만, 같은 아이디어입니다. 'n'이 z... 빈 벡터를 반환합니다. 그리고 'n'이 무언가의 후속자인 경우… 앞에 놓습니다. 복제… 즉, 꼬리에 대해 동일한 함수를 호출합니다. 여기에 전치가 있습니다. 벡터의 벡터가 있는 경우 기본적으로 열과 역할을 바꿔야 합니다. 여기서는 지점별 적용을 영리하게 사용하고 있기 때문에… 필요했습니다. 네, 아쉽게도 전치에 대해 설명할 시간이 없지만, 이 코드를 자세히 살펴보고 왜 작동하는지 확인하거나 모든 타입 'a'와 'a'의 1, 2, 3 요소에 대해 작동한다는 증명을 작성할 수 있습니다. 이 행렬을 전치하면 이 행렬이 됩니다. 1 1 1, 2 2 2, 3 3 3. 1 1 1, 2 2 2, 3 3 3. 이것을 어떻게 해결할까요? 해결되었습니다. 모든 타입과 이 타입의 3가지 구성원에 대해 해결되었습니다. 여기에 마지막 고차 함수가 있습니다. 'zipWith'... 'zipWith'를 모르신다면… 두 개의 벡터와 두 개의 인수를 사용하는 함수를 사용하여 해당 함수를 두 벡터에 적용합니다. 그래서 'zip'입니다. 'zip'은 바지의 지퍼와 같고 두 개의 가닥에서 하나의 것을 얻습니다. 몇 가지 디팬던트 타입을 더 살펴보겠습니다. 이제 진짜가 나타납니다. 이것은 시그마 타입이라고 합니다. 여기 이 글자… 타입 'a'의 무언가와 'a'의 요소에서 집합으로 가는 함수를 제공하면 집합을 반환합니다. 따라서 이것의 필드는… 첫 번째 필드는 타입 'a'를 가지고 있고 두 번째 필드는 첫 번째 필드에 적용된 함수… 즉, 첫 번째 필드의 요소에 적용된 함수를 가지고 있습니다. 무엇이든… 그리고 이 의존적인… 시그마 타입을 의존 곱이라고 부르는 이유는… 쌍이기 때문입니다. 항상 두 개의 값을 가지고 있습니다. 'proj₁'과 'proj₂'. 단, 두 번째 쌍의 타입… 두 번째… 요소의 타입은 첫 번째… 요소의 값에 따라 달라집니다. 그리고 여기에 그 예가 있습니다. 따라서 이것은 'n if false list of tt if true'라는 함수입니다. 부울을 가져와서 집합을 반환합니다. 'b'에 대해 패턴 매칭을 수행합니다. 거짓이면 자연수 타입을 반환하고 참이면 모든 자연수 'n'에 대해 'tt'의 'Vec'를 반환합니다. 그리고 여기에 이 함수를 사용하는 의존 곱의 값이 있습니다. 따라서 이것은 부울과 이 함수의 곱입니다. 두 번째 매개변수입니다. 따라서 이 함수는… 네, 두 번째 값의 타입은 무엇이 되어야 할까요? 첫 번째 값은 거짓이므로 자연수가 되어야 합니다. 그래서 이것이 컴파일됩니다. 두 번째 예는… 네, 이것은 'true true'이므로 두 번째 것의 타입은 이 'tt'의 목록입니다. 3개의 'tt'. 왜 이것을 사용해야 하는지 모르겠지만, 값에 따라 달라지는… 곱 타입을 가질 수 있다는 것을 보여주기 위한 것입니다. 표현식과 타입 시그니처를 가질 수 있습니다. 이제 정말 빨리 진행해야 합니다. 하지만 이것은 정말 대단합니다. 이것으로 많은 것을 할 수 있습니다. 여기에 5보다 큰 자연수 집합의 타입이 있습니다. 첫 번째 요소에 대한 증명인 두 번째 요소가 있는 의존 곱으로 정의하기만 하면 됩니다. 그리고 값 7이 5보다 크다는 증명을 구성할 수 있습니다. 증명은 'tt'가 될 것입니다. 왜냐하면 타입에서 계산되기 때문입니다. 하지만 첫 번째 요소가 3인 'greaterThan5'의 값을 생성할 수 없습니다. 이 구멍의 타입은 ⊥가 될 것입니다. ⊥의 값을 생성하는 것은 불가능합니다. 자연수에 대해 매개변수화할 수 있습니다. 따라서 여기에 'greaterThan n'이 있습니다. 값 'n'이 있습니다. 'greaterThan7' 타입입니다. 물론… 그렇습니다. 좋아요, 아직까지는 잘 따라오고 계신가요? 다룰 내용이 꽤 많기 때문에 마지막 부분은 빠르게 진행해야 합니다. 프로그램… 간단한 프로그램이지만… 그래도… 작은 행렬 라이브러리를 작성하는 모듈을 살펴보겠습니다. 자연수를 사용하고 이전에… 이전에 정의한 것을 사용하고 있습니다. 여기서 'Num'이라는 레코드를 정의할 것입니다. 집합을 가져와서 집합을 반환합니다. 이 집합에 대한 함수인 몇 가지 필드가 있습니다. 일부는 값이지만… 이것은 함수형 프로그래밍이므로 함수는 그냥… 값입니다. 그리고 이것은 Agda의… Agda의… Haskell의 타입 클래스에 대한 답변입니다. 혹시 모르시는 분들을 위해 말씀드리자면, Haskell의 타입 클래스… 런타임에… 이 타입에 대한… 딕셔너리로 축소됩니다. 이 함수의 구현은 이 타입에 대한 것입니다. 이 함수의 구현은 저 타입에 대한 것입니다. Agda는 이를 훨씬 더 명확하게 만듭니다. 이것은 모듈의 나머지 부분에서 이 레코드의 멤버를 범위로 가져오는 문법입니다. 여기에 인스턴스를 선언하는 방법이 있습니다. 인스턴스는 그냥… 이 레코드의 값입니다. 'Num'... 'Num'... 네, 이 집합, 자연수 집합에 대한 레코드의 모든 필드를 정의합니다. 그리고 이 집합, 실수 집합에 대한… 여기서 레코드를 만드는 문법은 코패턴이라고 합니다. 재밌는 표현이라고 생각합니다. 기본적으로 레코드의 타입을 제공하고… 그리고… 이 함수를 이 레코드에 적용한 것이 무엇인지 말합니다. 코패턴이라고 부르는 이유는 패턴… 패턴을 매칭할 때 패턴을 해체하여 '이 분기에 대해 이것을 수행합니다'라고 말하는 반면, 코패턴에서는 '모든 가능한 각도에서 이것을 구성하는 방법은 다음과 같습니다'라고 말합니다. 따라서… 설명하기가 좀 어렵지만… 기본적으로 필드를 기반으로 무언가를 구성하는 방법과 무엇이 될 수 있는지에 따라 무언가를 해체하는 방법입니다. 이중… 코패턴… 범주론… 하하… 그리고 이것이 인스턴스 인수임을 나타내는 방법입니다. 인스턴스 인수로 사용할 수 있습니다. 'instance'라는 키워드를 앞에 붙이기만 하면 됩니다. 그럼 행렬 타입과 행렬에 대한 함수를 살펴보겠습니다. 기본적으로 벡터의 벡터에 대한 새 타입입니다. 행의 개수와 열의 개수가 있습니다. 그리고 모든 타입… 에 대해… 그리고 두 행렬을 더할 수 있습니다. 치수가 같으면… 이것이 바로 이 함수가 정의하는 것입니다. 다시 말하지만 중위 연산자입니다. 따라서 두 행렬을 더하는 방법은… 네, 첫 번째 벡터를 첫 번째 벡터 레이어와 'zipWith'하고 두 번째 벡터를 'zipWith'하고 도중에 찾은 것을 더합니다. 이것이 바로 이 중첩된 'zipWith'가 하는 일입니다. 두 행렬에 적용합니다. 줄 바꿈이… 단어 줄 바꿈을 전환했었는데… 그렇습니다. 따라서 'a'의 행렬을 제공하면… 'a'의 다른 행렬을 제공하면… 'a'의 또 다른 행렬을 제공합니다. 같은… 치수를 가진… 행렬을 곱하는 것이 더 흥미롭습니다. 이제는… 치수가 'r'과 'c'인 행렬과 치수가 'c'와 'p'인 행렬을 곱하여 치수가 'r'과 'p'인 행렬을 생성할 수 있다고 말합니다. 매우 자연스럽게 표현됩니다. 구현 세부 사항에 대해서는 자세히 설명하지 않겠지만, 녹화를 다시 보고 코드를 자세히 살펴보면서 작동하는지 확인할 수 있습니다. 아… 이 코드를 자세히 살펴보라고 이미 말씀드렸네요. 왜냐하면 벡터에 대해 정의한 전치를 사용하고 있기 때문입니다. 따라서 실제로는 두 개의 코드 레이어를 자세히 살펴봐야 합니다. 여기에 몇 가지 다른 함수가 있습니다. 그냥… 벡터를 제공하면 열 행렬을 구성합니다. 즉, 단일 열이 있는 행렬입니다. 따라서 'n'... 행이 있습니다. 벡터의 길이이고 열은 1개입니다. 그리고 행렬에 대한 벡터… 행은… 행이 1개이고 열이 있습니다. 그리고 이것은 전치의 동의어일 뿐입니다. 하지만 수학 표기법으로 작성된 행렬을 본 적이 있다면… 'T' 제곱이 있습니다. 깔끔하네요. 네, 이러한 중위 선언이 곳곳에 있습니다. 이것은 연산자가 왼쪽으로 결합할지 오른쪽으로 결합할지 나타냅니다. 이 경우에는 인수가 하나이므로 의미가 없습니다. 그리고 우선순위와 얼마나 밀접하게 결합해야 하는지… 네, 작은 행렬 라이브러리입니다. 행렬을 더하고 곱하고 벡터로 변환할 수 있습니다. 간단한 것들입니다. 그리고 행렬의 의사 역행렬을 구하고 싶습니다. 이제 이것은 까다로운 연산입니다. 행렬을 역행렬로 바꿔본 적이 있다면 LU 분해와… 행렬이 특이 행렬이 아님을 확인하는 것이 간단한 알고리즘이 아니라는 것을 알 것입니다. 따라서… 린디 효과로 돌아가서… Agda는 코드를 얼마나 신뢰할 수 있는지, 즉 코드가 정확한지 여부에 신경 쓰는지 여부에 따라 린디 효과를 활용할 수 있는 방법을 제공합니다. 오랫동안 사용되어 온 코드를 사용하고 정확하다고 믿을 수 있습니다. FFI를 사용하면... Agda는 Haskell로 컴파일됩니다. 이것이 Agda가 궁극적으로 실행되는 방식이고 우리가 사용할 수 있도록 화면에 무언가를 생성하는 방식입니다. 그리고 Agda에는 FFI가 있기 때문에 Agda에서 Haskell 코드를 호출할 수 있습니다. 또한 Haskell에서 Agda 코드를 호출할 수도 있습니다. 흥미롭습니다. 그리고… 이 부분에 대해서는 딱히 할 말이 없습니다. 'trustMe'가 사용되는 것을 볼 수 있을 것이고, 이것은 바로… '모든 타입 안전성은 잊어버리고 저를 믿으세요. 이것은 작동합니다.'라는 지점입니다. 참고로 이것은 실제 라이브러리 이름입니다. 패키지 이름입니다. 'trustMe'라고 합니다. 그리고 거기에 모든 것이 다른 모든 것과 같다는 증명이 있습니다. 저를 믿으세요. 정확합니다. 따라서 이것이 작동하는 방식입니다. 아… 단어 줄 바꿈을 다시 설정해야겠네요. FFI를 사용하기 위한 프라그마에는 세 가지 유형이 있습니다. 따라서 이것은 컴파일러에게… 코드의 이 부분을 컴파일할 때 이 Haskell 코드를 삽입하라고 지시합니다. 'HSMatrix'를 가져옵니다. 그것은 무엇일까요? 여기 또 다른 프라그마가 있습니다. 'compile' 프라그마… 이 'postulate'... 논리학에서 'postulate'는 우리가 그냥… 사실이라고 말하는 것입니다. '이 명제를 가정해 보겠습니다.' 'postulate'는… 공리와… 그냥… 사실이기 때문에 사실인 것들의 자리를… 차지하려고 합니다. 제 생각에는 'postulate'와 공리 사이에 차이가 있는 것 같은데, 저는 잘 모르겠습니다. 하지만 Agda에서 아무것도 없는 상태에서 무언가를 만들어내는 방법입니다. 그리고 이것이… FFI에 지시하는 내용입니다. 실수의 목록의 목록을 가져와서 실수의 목록을 반환하는 이 'postulate'가 보이면 'invertMatrixAsList'로 설정합니다. 이것은 Haskell 코드입니다. 이것이 실제로 변환될 것입니다. 이것을 컴파일하는 대신… 보일 때마다 이 Haskell 코드와 같게 만듭니다. 여기에는 목록을 벡터로, 벡터를 목록으로 변환하는 몇 가지 변환 코드가 있습니다. 이 부분을 제외하고는 모두 건너뛰어야 할 것 같습니다. 여기 'trustMe' 증명… 네, 걱정하지 마세요. 저는… 이것은 작동할 것입니다. 저를 믿으세요. 저는 그 이름이 정말 마음에 듭니다. 따라서 'postulate'를 호출하기 위해 'fromListOfLists'를 사용합니다. 이것은 '-1' 제곱인 역행렬 연산자입니다. 먼저 변환 함수를 사용하여 행렬을 목록으로 변환한 다 역행렬로 바꿉니다. 'postulate'를 호출하여 역행렬로 바꿉니다. 그런 다음 'trustMe'를 다시 전달하여 얻은 것을 변환하여… 치수가 일치하는지 확인합니다. 따라서… 모든 'n'에 대해 정사각형 행렬을 제공하면… 치수가 'n' 곱하기 'n'인 행렬을 제공하면 'n' 곱하기 'n'을 반환합니다. 따라서 이제 Agda 함수입니다. 이것은 그냥… Agda 수준에서 작동합니다. 증명은… 또는 항은… 'n'이… 행렬이 정사각형이고 입력이 출력과 같다는… 증명에 대해 테스트될 것입니다. 등등. 그리고 여기에 행렬을 표시하는 몇 가지 코드가 있습니다. 다시 말하지만, 표준 라이브러리를 사용하고 있습니다. 네, 그냥… 별거 없습니다. 벡터를 재귀적으로 순회하고 쉼표로 구분합니다. Haskell과 매우 유사해 보일 것입니다. 그리고… 행렬을 표시하려면 'showVec'를 사용하기만 하면 됩니다. 마지막으로 살펴볼 모듈은… 메인 모듈입니다. 예! 이제 프로세서를 워밍업하는 것이 아니라 실제로 무언가를 실행하고 있습니다. 여기에서 몇 가지 가져오기를 수행합니다. Agda와 IO의 관계는 예상대로… 복잡합니다. 여기 이 'level0'과 같은… 몇 가지 문법적인… 문법적인 것뿐만 아니라 몇 가지 노이즈가 있습니다. 이미 IO를 실행하고 있음에도 불구하고 IO 호출을 실행해야 한다는 사실… 무슨 일이 일어나고 있는 걸까요? 너무 신경 쓰지 마세요. 실제로는 이 'io.run'이나… 레벨… 레벨 호출을 보지 말아야 합니다. 이것은 행렬을 출력하는 IO 호출일 뿐입니다. 행렬을 제공하면 ⊤를 반환하는 IO 연산을 제공합니다. 그리고 여기에 메인 함수가 있습니다. 행렬 'm'을… 이 행렬, 2 6 3… 4로 설정합니다. 'm⁻¹'을 역행렬로 설정합니다. 그리고… 네, 여기서 볼 수 있는 것은… 먼저 행렬을 출력하고… 그 다음 역행렬을 출력하고… 그 다 행렬과 역행렬을 곱한 것을 출력합니다. 그리고 이것은 단위 행렬을 반환해야 합니다. 운이 좋다면요. 따라서 여기에 작은 빌드 명령이 있습니다. 이것은… Nick의 셸 스크립트로 생성되었습니다. 코드를 컴파일하고… 연결합니다. 그리고 이 코드를 실행할 수 있습니다. 그리고… 여기 있습니다. 행렬 'm'은 2 6 3 4이고 역행렬은 -0.4… 등등… 그리고 역행렬을 곱하면… 이런… 세상에… 맞았나요? 네, 따라서 여기에 1과 0.4가 있고… 10의 -16제곱과… 10의 -16제곱… 그리고 1. 따라서 이것은 실제로 부동 소수점 오류를 뺀 1 0 0 1입니다. 단위 행렬입니다. 그리고… 네, 이것은… 기본적으로 내용입니다. 여기에 작은 부록을 추가하여 Haskell 모듈이 어떻게 생겼는지 보여드리겠습니다. 그리고 여기 있습니다. 실제로는 Singletons를 사용하지 않습니다. 이것은 다음 강연에서 다루겠습니다. 하지만 이것은 외부 라이브러리를 사용하고 있습니다. 이 Haskell 파일은… Hackage에서 가져온 외부 라이브러리를 사용하고 있습니다. 'hmatrix'라고 합니다. 그리고 이 라이브러리는 의사 역행렬 알고리즘을 구현합니다. 이것이 바로 코드의 린디 부분입니다. 해당 코드는 공개되어 있고 테스트를 거쳤으며 오랫동안 실행되어 왔습니다. 더… 네, lapack과 blas와 같은 더 잘 테스트된 코드에 의존합니다. 알고리즘… 그리고 여기 이 작은 모듈은… 오랫동안 사용되어 온 린디 코드를 신뢰하는 세계와… fum... 매우 타입 안전한 Agda의 정리… 정리로 가득 찬 세계를 연결하는 역할을 합니다. 그리고… 제가 마지막으로 말씀드리고 싶은 것은… 정확성을 표현하는 것이 편리할수록… 즉, 해당 타입에서 본 많은 것들이 매우 자연스럽습니다. '15는 11 + 4와 같습니다.' 누구나 해당 코드를 읽고 이해할 수 있습니다. 정확성을 표현하는 것이 편리할수록… 제 생각에는 편의성과 정확성 사이의 트레이드오프가 더욱 무의미해집니다. 즉, 의도를 컴퓨터가 검증 가능한 정확한 것으로 변환하는 데 드는 노력이 줄어듭니다. '이것이 정확한지 확인하기 위해 몇 개의 테스트 레이어와 얼마나 많은 타입 푸를 사용해야 할까?'라고 걱정할 필요가 줄어듭니다. 그리고 제 생각에는 Agda가 여기서 중요한 역할을 합니다. 왜냐하면… 제 생각에는… 코드를 작성할 때 우리가 실제로 의미하는 바를 자연스럽게 표현할 수 있게 해주는 매우 아름다운 언어이기 때문입니다. 저는 그 단어를 신중하게 사용하고 있습니다. 그리고 제가 여러분을 설득했거나 적어도… 그럴듯하게 들리도록 만들었기를 바랍니다. 이것으로 Agda 소개를 마치겠습니다. 감사합니다.

다시 한번 감사합니다, Andrea. 네, 저는… 모든 것을 이해하지는 못했습니다. 노력했습니다. 두 번 봤는데… 질문 있으신가요? 네, 질문이 있습니다. 마이크를 전달해 주세요.

행렬에 요소를 잘못된 위치에 추가하면 타입이 어떻게 되는지 보여주시겠어요? 네, 물론입니다. 마이크가 엉켰네요. 네, 보여드리겠습니다. 전치의… 전치 증명에서 말씀하시는 건가요? 아니면… 제공하려고 할 때… 네, 어떨까요? 만약… 만약… 아… 네, 좋은 질문입니다. 여기에 요소를 추가하면 어떻게 될까요? 네, 네. 따라서 타입 오류가 어떻게 표시되는지… 따라서 여기서… 잘못 구성된 행렬을 추가했습니다. 행 중 하나에 열이 2개 있고 다른 행에는 열이 3개 있습니다. 따라서 이 모듈을 로드하려고 하면… 네, 이미 무엇을 찾고 있는지 알고 있지 않으면 읽기가 좀 어렵지만, 기본적으로 진실을 말하고 있습니다. 무언가의 후속자는… 0과 같지 않습니다. 이 값을 구성할 때… 첫 번째 벡터의 패턴 매칭에 도달하면 매칭의 양쪽이 0인지 확인하려고 하고 둘 중 하나는… 무언가의 'Succ'이 될 것이고, 'Succ'은 0이 아닙니다. 하지만… 네, 더 나은… 타입 오류는… 이렇게 하면 나타날 것입니다. 왜냐하면… 이런… 따라서 이것은 잘 구성된 행렬이지만… 정사각형이 아닙니다. 따라서 이제… 이제 훨씬 더 나은 오류입니다. '3은 2와 같지 않습니다.' 표현식 'Matrix Float'를 확인하고 있습니다. 이것들을 제대로 가져왔다면 조금 더 보기 좋았을 것입니다. 하지만 '3은 2와 같지 않습니다.' 왜냐하면 행은 2개이지만 열은 3개이기 때문입니다. 따라서… 행렬이 정사각형이 아니기 때문에… 역행렬로 바꿀 수 없습니다. 감사합니다.

다른 질문 있으신가요? 모두 이해하셨나요? 네, 혼자셨네요. 네, 죄송합니다. 아, 저쪽에 질문이 있네요. 네, 마이크를 전달해 드리겠습니다. 네, 발표 잘 들었습니다. 매우 흥미로웠습니다. 질문은… 좀 이상하게 들릴 수도 있지만… 이런 유형의… 프로그래밍의 적용… 즉… 실제로 이러한 기술을 사용해야 할… 수요가 있는 곳이… 네, 좋은 질문입니다. 그리고 Agda를 구체적으로 사용하는 회사는 적어도 한 곳 알고 있습니다. IOHK라는 회사인데, 지금은 IOG로 이름을 바꿨습니다. 블록체인을 하고 있고… 블록체인 간의 프로토콜을 만들고 있습니다. 따라서… 작성하는 코드가 정확해야 하고 Agda를 사용하여 정리를 증명합니다. 하지만 저는 Agda를 사용하여 개발된 프로그램을 알고 있습니다. 예를 들어 검증된 C 컴파일러가 Agda를 사용하여 개발되었다고 확신합니다. 그리고 그것은… 'CompCert'라고 합니다. 제 생각에는 항공 소프트웨어와 같은 몇 가지 중요한 애플리케이션에서 사용됩니다. 오류가 발생하면 사람이 죽을 수 있습니다. 네, 두 번째 부분은 확실하지 않지만… 90% 확신합니다. Agda… 와 관련된 것입니다. 네, 좋아요.

Q: 저도 질문이 하나 있습니다. 어떻게 Agda를 접하게 되었나요?
A : Agda를 접하게 된 계기는 Haskell에 관심이 있었고… 석사 학위를… 복잡 적응 시스템으로 하고 있었습니다. 이것은… 물리학과 컴퓨터 과학이 혼합된 분야인데… 제 생각에는… 좀 특이한 분야입니다. 하지만 제 생각에는 근본적인 질문은 '사물이 어떻게 동일한가?', 즉 '이러한 것들의 기본 구조는 무엇인가?'입니다. 따라서 Haskell에서 본 그 질문을 통합하고 싶었습니다. Haskell은… 타입 클래스와 여러 타입에 걸친 균일한 동작… 그리고 모든 것… 그래서 그 분야에서 더 발전된 것을 찾게 되었고… 결국… 디팬던트 타입을 접하게 되었습니다. 그리고 석사 과정은 Agda가 개발된 샬머스에서였기 때문에… 네, Haskell에서 범주론, 디팬던트 타입으로… 복잡 시스템과 결합하게 되었습니다. 그리고 Agda는 자연스러운 선택이었습니다.

그리고… 샬머스… 좋아요. 감사합니다. 다른 질문 있으신가요? 없으시다면… Andrea에게 다시 한번 감사드립니다. 네, 감사합니다.

)