Agda from Nothing - Scott Fleischman.mdx

2016-10-04

Part 1 : https://www.youtube.com/watch?v=-i-QQ36Nfsk

Part 2 : https://www.youtube.com/watch?v=XprGyVWXwks

제 이름은 스콧 플라이시먼이라고 합니다.

최근에 혼자서 아그다를 가지고 정말 열심히 해킹을 해 왔는데요, 시작하기 정말 어려운 언어입니다.

아그다 자체가 그렇게 복잡해서 그런 건 아니라고 생각해요.

아그다를 좋아하고 정말 사용하는 사람들이 수학이나 타입 이론 같은 걸 전공하는 대학원생들이기 때문이라고 생각합니다.

그리고 그들은 이런 추가적인 것들을 다 가지고 있고, 그들이 사용하는 예제들은 제가 배우고 싶어 하지만 아직 배우지 못한 것들에서 나옵니다.

그래서 핵심에서 정말 무슨 일이 일어나고 있는지 알기가 더 어렵죠.

그래서 밥 하퍼의 강좌를 들었고, 많은 튜토리얼을 읽었고, 오리건 여름 학교 프로그래밍 언어 세미나 같은 것도 봤고, 많이 읽었습니다.

그래서 여러분과 공유하고 싶은 것은 박사 학위를 받을 수 있을 정도로 방대한 주제에 빠지지 않고 아그다에 대해 배우고 프로그래밍을 즐기는 것입니다.

저에게 아그다는 가장 좋아하는 프로그래밍 언어입니다.

학부에서 컴퓨터 과학, 수학, 철학 논리를 공부했는데, 아그다는 이 세 가지를 모두 통합합니다.

그래서 프로그래밍을 할 수 있고, 이런 프로그래밍 모드를 가질 수 있거나, 논리적 증명을 할 수 있고, 이런 논리적 측면을 가질 수 있거나, 수학에 대한 것들을 증명할 수 있고, 집합 이론 이외의 수학에 대한 대안적인 기초를 가질 수 있습니다.

그리고 그것은 모두 동일한 시스템입니다.

그래서 제가 아그다를 좋아하는 이유입니다.

아그다 위키에서 말했듯이, 아그다는 의존적으로 타입이 지정된 함수형 프로그래밍 언어입니다.

아그다 자체는 또한 증명 보조 도구이기 때문에 증명을 작성하는 데 도움이 될 것입니다.

그리고 직관주의적 타입 이론을 기반으로 하기 때문에 그 뒤에 꽤 오래된 이론이 있습니다.

1908년 버트런드 러셀이 집합 이론을 사용하여 수학에 대한 형식적인 시스템을 만들려고 시도하면서 시작되었다고 할 수 있습니다.

하지만 그러면 이런 역설을 발견하게 됩니다.

자신을 포함하지 않는 모든 집합의 집합은 마치 자신을 포함하는지 아닌지처럼 보입니다.

둘 다 될 수 있는 것 같습니다.

그래서 그는 이 타입 이론에 대한 아이디어로 시작했습니다.

어떤 타입은 자신에 대해 말할 수 없기 때문에 집합은 더 이상 자신을 포함하는 집합에 대해 말할 수 없습니다.

이 계층 구조는 계속 올라갑니다.

물론 1930년대에 알론조 처치가 람다 미적분학을 사용하여 순수한 함수만 사용하여 수학, 숫자 등을 모두 인코딩할 수 있다는 것을 보여주었습니다.

대체의 개념은 정말 매혹적인 시작이지만, 1970년대에 마틴 뢰프가 이 이론을 만들면서 타입 이론이 정말로 완성되었습니다.

수학의 기초이기도 하지만 프로그래밍 언어로 볼 수도 있습니다.

다른 방식으로 보고 해석할 수 있는 동일한 시스템과 같으며, 그것이 바로 아그다입니다.

아그다는 컴퓨터가 여러분을 위해 증명을 확인할 수 있도록 타입 이론을 구현한 것입니다.

그래서 아그다 프로그램을 작성하고 타입 검사를 하면 뭔가 성취한 것 같은 느낌이 듭니다.

왜냐하면 적어도 여러분이 말한 것과 일치한다는 것을 증명했기 때문입니다.

글쎄, 여러분이 말한 것이 여러분이 생각한 것과 일치하지 않을 수도 있지만, 프로그램의 구현은 실제로 일치합니다.

아그다 자체는 1999년 카타리나 코콘드가 처음 작성했습니다.

2007년 노렐라가 박사 학위 논문을 위해 완전히 다시 작성했고, 아그다에 대한 메타 이론을 작성하고 증명했습니다.

그래서 사람들이 아그다라고 말할 때는 실제로 이 아그다2를 의미합니다.

좋아요, 핵심 주제는 그렇게 많지 않습니다.

귀납적 타입을 만드는 것입니다.

귀납적이라는 것은 자연수와 같이 잠재적으로 무한하지만 항상 실제로 유한하다는 것을 의미합니다.

숫자를 주면 항상 더 큰 숫자를 만들 수 있지만, 항상 우리가 이야기하고 있는 유한한 숫자를 가지고 있습니다.

오늘은 코드 귀납적 타입에 대해서는 다루지 않겠습니다.

함수, 특히 전체 함수, 그래서 우리는 항상 입력 집합이나 타입의 모든 것을 입력으로 처리하고, 동등성을 처리합니다.

그리고 동등성은 우리에게 증명의 개념을 제공합니다.

어디에나 존재합니다.

그래서 제가 할 일은 아그다에서 부울을 사용하여 정말 기본적인 함수형 프로그래밍을 하는 것이고, 바로 의존적 타입으로 넘어가서 동등성과 우리가 만든 타입과 함수에 대한 몇 가지 증명에 대해 이야기할 것입니다.

그래서 정말 쉽고 나서 꽤 깊이 들어갈 것입니다.

길을 잃을 수도 있지만, 다시 돌아와서 좀 더 쉬운 자연수로 돌아가서 그에 대한 몇 가지 증명을 할 것입니다.

동등성은 이미 어디에나 있겠지만, 아그다가 무료로 제공하는 동등성의 몇 가지 깔끔한 속성이 있습니다.

그리고 시간에 따라 조금씩 방향을 바꿀 것입니다.

마지막 두 가지를 자세히 다룰 수 있기를 바랍니다.

그렇지 않으면 적어도 몇 가지 기본적인 것들을 할 수 있을 것입니다.

논리, 특히 구성적 논리.

제가 고전 논리와 대조적으로 구성적 논리라고 말할 때, 사람들이 일반적으로 대조하는 고전 논리는 배중률의 법칙을 얻습니다.

즉, 명제는 참이거나 거짓이라는 것입니다.

그리고 구성적 논리는 그 전제로 시작하지 않지만 부정하지도 않습니다.

그리고 아그다에서 증명을 보여드릴 수 있기를 바랍니다.

명제가 참이거나 거짓인지 알 수는 없지만, 명제가 참이거나 거짓이 아니라는 것은 사실이 아닙니다.

이중 부정과 같습니다.

그리고 사람들이 아그다로 하는 일반적인 일은 목록의 길이가 항상 존재하는 목록에 대한 정말 이상한 이름인 벡터를 보여주는 것입니다.

그리고 그것이 제가 다루고 싶은 내용입니다.

그리고 제가 그렇게 할 방법은 라이브 코딩을 하고 그것을 진행하는 것입니다.

그리고 꽤 많은 사람들이 있기 때문에 모든 사람이 아그다를 설치했다고 가정하지 않겠지만, 따라오고 있다면 중간에 연습할 시간을 줄 것입니다.

그리고 저는 조용히 그것들을 진행하고 몇 분을 줄 것입니다.

그러면 아그다가 있으면 뭔가를 해킹할 수 있지만, 그렇지 않으면 따라올 수 있고 저는 그것들을 논의할 것입니다.

하지만 대체로 라이브 코딩을 하고 질문이 있으면 소리쳐서 물어보세요.

가끔 집중을 하다 보면 잘 안 들릴 수도 있지만, 소리쳐서 물어보면 설명해 드리겠습니다.

그리고 또 한 가지 말씀드리고 싶은 것은 이 강연을 몇 번 해봤는데, 프로그래밍에 대해 전혀 모르는 몇몇 언어학자 동료들과 함께 해봤는데, 그들은 한동안 따라올 수 있었고, 어느 시점이 되면 모든 새로운 추상적인 개념들이 합쳐져서 길을 잃지만, 꽤 잘 따라올 수 있었습니다.

그래서 저는 정말 만족했습니다.

그리고 개발자 동료들과 함께 이 강연의 몇 가지 버전을 진행해 봤는데, 실제로 비슷한 일이 일어납니다.

그들 중 누구도 실제로 함수형 프로그래머가 아니었기 때문에 새로운 것들이 많았지만, 지금까지 받은 피드백을 보면 모두 즐거워하는 것 같았습니다.

좋아요, 핵심 주제 중 하나는 귀납적 타입입니다.

모두에게 충분히 크게 보이나요? 읽을 수 있나요? 좋아요, 훌륭합니다.

그게 뭐죠? 저는 아그다2.51을 사용하고 있습니다.

대부분의 경우 이전 버전을 사용해도 괜찮을 것입니다.

하지만 제가 설정할 한 가지 옵션은 명시적입니다.

그게 뭐죠? 여기에 넣지 않았어요.

여기에 있습니다.

연습 문제 중 하나에서 맨 위에 이 정확한 분할 옵션을 사용하고 있다는 것을 알 수 있을 것입니다.

이전 버전에서는 사용할 수 없습니다.

그 장점은 함수를 정의할 때 각 정의 줄, 즉 정의하는 각 경우가 정의상 동일하도록 보장한다는 것입니다.

왜냐하면 아그다가 경우를 분할하기 때문입니다.

잠시 후에 보여드리겠지만, 대체로 이전 버전을 사용해도 괜찮을 것입니다.

실제로 테스트해 보지는 않았지만, 연습 문제를 시도하면 그런 것들 때문에 오류가 발생할 것입니다.

그리고 아그다2.51에는 이런 내장 기능이 있습니다.

대부분의 경우 기본 사항을 모두 다시 정의하기 때문에 사용하지 않는다고 생각합니다.

아마도 목록 연습 문제에서는 내장 기능을 몇 가지 사용했을 것입니다.

하지만 대체로 이전 버전을 사용해도 괜찮을 것입니다.

좋아요, 타입.

귀납적 타입을 만들어 보겠습니다.

시작하기에 가장 좋은 방법은 부울이라고 생각합니다.

그래서 이름을 지정합니다.

데이터는 키워드입니다.

부울이고 집합입니다.

이 강연에서는 타입과 집합의 차이점에 대해 걱정하지 않겠습니다.

상호 교환적으로 사용할 것입니다.

몇 가지 미묘한 차이점에 대해 꽤 지저분한 철학적 논의를 할 수 있지만, 우리의 목적상 집합은 타입입니다.

그래서 이제 집합의 요소 또는 생성자라고 부르는 것을 정의할 것입니다.

참은 부울입니다.

그리고 거짓은 부울입니다.

집에서 따라 하고 있다면 아그다 이맥스 모드에서 con은 Ctrl+C, Ctrl+L을 눌러 로드하면 파일의 타입이 검사됩니다.

저는 거의 항상 그렇게 합니다.

아마도 편집기가 자동 저장하거나 항상 어느 정도 자동 로드해야 한다고 생각합니다.

20~30년 전에 자동 저장이 기본값이 아니었을 때가 생각나네요.

항상 끊임없이 저장해서 뭔가를 잃어버리지 않도록 했죠.

좋아요, 그러면 핵심 표기법은 이 콜론입니다.

그래서 부울은 집합이거나 집합 타입을 가진다고 읽을 수 있습니다.

참은 부울 타입을 가지고 거짓은 부울 타입을 가집니다.

그래서 이제 우리는 집합을 만들었고 그 안에 요소가 있습니다.

하지만 집합도 부울이라는 이름으로 이야기할 수 있습니다.

글쎄, 집합이니까 모든 것에는 그 위에 뭔가가 있는 것 같습니다.

그리고 뭔가의 타입이 무엇인지 물어보는 방법은 Ctrl+C, Ctrl+D를 눌러 타입을 추론하거나 유추하는 것입니다.

그리고 맨 아래에 표현식이 있습니다.

부울을 입력하면 부울이 집합이라고 알려줍니다.

그리고 Ctrl+C, Ctrl+D를 다시 누르고 참을 입력하면 참이 부울이라는 것을 유추합니다.

꽤 쉽습니다.

이렇게 같은 것을 쓸 수 있는 구문적인 방법이 있습니다.

하지만 모두 정말 간단한 요소라면, 이것들을 생성자라고 합니다.

참과 거짓 데이터 생성자는 한 줄에 넣을 수 있습니다.

특히 10개 정도 있으면 꽤 길어질 수 있습니다.

음, 좋아요.

다시 돌아올 수도 있는 몇 가지 퇴화된 경우가 있습니다.

빈 경우로 확실히 돌아올 것이지만, 정확히 하나의 요소만 있는 타입을 만들 수 있습니다.

단위이고 이것은 유용합니다.

이것을 만드는 방법은 하나뿐이기 때문에 나중에 유용합니다.

그리고 아마도 생각조차 하지 못했을 정말 퇴화된 경우는 공집합입니다.

공집합의 뭔가를 만들 수 있는 방법은 없습니다.

이상하게 들릴 수도 있지만, 부정의 증명에 매우 유용합니다.

왜냐하면 기본적으로 요소를 만들 수 있다면 명제가 참이라고 말하기 때문입니다.

그리고 만들 수 있다면 거짓입니다.

그래서 아그다는 뭔가에 대한 증명을 만들 수 있게 해 줄 것입니다.

해당 타입의 뭔가를 만들 수 있거나 만들 수 없다면 거짓입니다.

그래서 어떤 의미에서 이것은 진실과 같습니다.

그리고 때로는 사람들이 tt를 참으로 줄여서 단위를 줄여 쓰는 것을 볼 수도 있습니다.

그리고 공집합은 사람들이 이런 것들에 다른 이름을 붙이는 또 다른 이름입니다.

void, 0이라고도 합니다.

왜냐하면 만드는 방법이 0가지이기 때문입니다.

그리고 어떤 사람들은 이것을 1이라고도 합니다.

왜냐하면 해당 집합을 만드는 방법이 정확히 하나이기 때문입니다.

그리고 그 경우 이것은 2가 될 것입니다.

왜냐하면 만드는 방법이 두 가지이기 때문입니다.

음, 그래서 이런 것들을 때때로 사람들이 그 수준에서 작업하는 것을 볼 수 있습니다.

음, 지금은 부울로 돌아가겠습니다.

좋아요, 함수를 몇 가지 만들어 보겠습니다.

여기에 함수에 대한 내용이 있나요? 음, 여기 어딘가에 슬라이드가 있는 것 같습니다.

좋아요, 말씀드렸듯이 타입을 만드는 방법은 집합이나 타입에 이름을 지정하고 해당 이름이 여기 아래쪽에 나타납니다.

그리고 이것들은 모두 다른 생성자입니다.

좋아요, 함수.

음, 한 가지 말씀드리고 싶은 것은 뭔가에 이름을 지정하고 싶다면 부울에 특정 이름을 지정하고 싶다고 말할 수 있습니다.

그래서 mybull이라고 부르겠습니다.

좋아요, 거기에 있습니다.

이름을 지정하는 모든 것은 타입과 항을 가지게 됩니다.

그래서 mybool은 부울 타입을 가지고 어떤 부울인지 묻습니다.

글쎄, 이 경우 mybool은 참이 될 것입니다.

음, 그리고 아그다에게 mybool이 무엇으로 줄어드는지 알려달라고 요청할 수 있습니다.

그래서 Ctrl+C, Ctrl+N을 누르고 표현식을 입력하면 최대한 줄이려고 할 것입니다.

mybool이 참과 같다고 말했으니까 mybool을 입력하면 참으로 줄어들 것입니다.

꽤 간단하지만, 함수를 만들면 더 흥미로워질 것입니다.

그래서 첫 번째 함수를 만들면 타입을 가지게 됩니다.

이제 함수는 어떤 의미에서 특별합니다.

화살표를 사용한다는 것입니다.

그래서 왼쪽에 있는 것은 집합의 이름이 되고 오른쪽에 있는 것도 집합의 이름이 될 것입니다.

그래서 부울에서 부울로 함수를 만들 수 있습니다.

그렇게 화살표를 만들 수 있습니다.

음, 아그다는 유니코드를 정말 잘 지원하기 때문에 멋진 유니코드 문자를 입력할 수 있는 재미있는 방법을 많이 제공합니다.

그래서 백슬래시를 입력한 다음 to를 입력하면 작은 유니코드 화살표를 얻을 수 있습니다.

또는 때로는 백슬래시 r을 입력하고 맨 아래에서 다양한 화살표를 선택할 수 있습니다.

함수에 사용할 수 있는 것은 첫 번째 화살표뿐이지만, 원하는 대로 다른 화살표를 사용할 수 있습니다.

네.

이 저장소로 이동하면, GitHub로 이동하여 아무것도 없는 아그다를 검색하면 여기에 몇 가지를 요약해 놓았습니다.

그리고 아그다 문서로 이동하면 모두 나열할 수 있습니다.

하지만 이것은 입력하는 내용과 얻는 내용입니다.

하지만 물론, 음, 잊어버리면 알려주세요.

그렇게 하지 않으려고 노력하겠지만, 가끔은 유니코드 화살표를 참을 수 없을 때가 있습니다.

실제로 필요하지 않습니다.

둘 다 사용할 수 있습니다.

그래서 이것도 잘 작동할 것입니다.

빼기 기호와 초과 기호입니다.

좋아요, 어디까지 했죠? 질문.

네.

음, 부울 예제의 경우 참과 거짓이 강의 순서대로 되어 있는지, 집합이라는 것은 알지만 이 특정 연습 문제의 경우 거짓이 참보다 앞에 있는 것이 중요한지 묻는 것입니다.

아니요, 그렇게 중요하지 않습니다.

음, 핵심 언어라고 부르는 것의 목적에는 그렇지 않습니다.

하지만 리플렉션이나 뭔가를 사용하면 열거할 수 있을지도 모릅니다.

기억이 안 나네요.

하지만 일반적으로는 아니요.

그냥 이름입니다.

좋아요.

음, 그러면 함수를 만들 때 자동으로 추출하는 경우 순서가 중요한지 묻는 것입니다.

음, if를 다루면 질문에 대한 답을 알 수 있을 것입니다.

언어에는 기본적으로 if가 없습니다.

좋아요, 함수를 만드는 방법은 일반적으로 패턴 매칭이라고 하는 것입니다.

왼쪽에서 각 경우를 처리해야 합니다.

그래서 참인 경우를 처리해야 합니다.

음, 아마도 그리고 함수의 거짓인 경우를 처리해야 합니다.

그래서 이것은, 그래서 아이디어는 부울 입력을 제공하고 부울 출력을 제공하는 것입니다.

그래서 참을 전달하면 참을 다시 얻고 거짓을 전달하면 거짓을 다시 얻습니다.

음, Ctrl+C, Ctrl+N을 눌러 표현식을 실행하거나 정규화하거나 줄일 수 있습니다.

그리고 myfunction이라는 표현식을 입력합니다.

그리고 참이라는 인수를 제공하면 Enter 키를 누르면 참으로 줄어듭니다.

꽤 간단하지만 사람들은 일반적으로 이것을 항등 함수라고 부릅니다.

왜냐하면 입력한 것을 그대로 돌려주기 때문입니다.

만들 수 있는 또 다른 함수는 not입니다.

not은 참을 받아서 거짓을 반환하고 거짓을 받아서 참을 반환합니다.

그래서 Ctrl+C, Ctrl+L을 눌러 로드하고 조금 테스트하고 싶다면 Ctrl+C, Ctrl+N을 눌러 정규화하고 not false를 입력하면 참으로 바뀝니다.

아니요, 참으로 바뀝니다.

그리고 not, 음, 참은 거짓으로 줄어듭니다.

음, 이것이 제공하는 몇 가지 좋은 점이 있습니다.

음, 아그다가 제공하는 좋은 점입니다.

그래서 음, 항등 함수가 마음에 들지 않을 수도 있습니다.

모든 경우가 무엇인지는 중요하지 않습니다.

왜냐하면 같은 것을 그대로 돌려줄 것이기 때문입니다.

그래서 왼쪽에 있는 것에 이름을 지정할 수 있습니다.

그리고 오른쪽에 있는 것은 그냥 반환할 수 있습니다.

그래서 이제 항등 함수는 부울을 입력으로 받습니다.

x라고 부르겠습니다.

그리고 저는 그냥 그 부울을 그대로 돌려줄 것입니다.

그래서 표현식을 다시 줄이면, 항등 함수에 거짓을 전달하면 물론 거짓을 다시 얻습니다.

조금 더 크게 말씀해 주시겠어요? 네, 할 수 있습니다.

지금 당장은 그렇게 하지 않겠지만, 곧 다형성을 하는 방법을 보여드리겠습니다.

하스켈이나 ML과는 다른 맛이 있습니다.

왜냐하면 모든 것이 매개변수이기 때문입니다.

그래서 기본적으로 아그다의 다형성 함수는 실제로 첫 번째로 제공하는 것이 집합이고 다음으로 제공하는 것이 해당 집합의 이름인 의존적 함수입니다.

잠시 후에 보여드리겠습니다.

음, 컴파일러를 다시 실행하면 건너뛰고 있다고 합니다.

그래서 기본적으로, 아, 그렇게 되는군요.

건너뛰고 있다고 하면 변경하지 않았다는 의미입니다.

음, 명령줄에서 실행할 때, 네, 글쎄, 다른 것들을 건너뛸 수도 있습니다.

확실하지 않아요.

음, 제가 들으면, 너무 작네요.

음, 아그다를 실행하고 아무것도 없는 활성이라고 말하면, 음, 글쎄, 이맥스에서 로드했다면 이 .agdai 파일을 만들고 있을 것입니다.

이 파일은 기본적으로 타입 검사 정보의 이진 직렬화된 형식입니다.

그래서 아그다에서 이미 로드했다면 Ctrl+C, Ctrl+L을 눌렀고 명령줄로 가서 그렇게 하려고 하면 이미 컴파일되었기 때문에 건너뛸 것입니다.

이맥스에서 로드하면 이미 컴파일되었기 때문에 다시 확인할 필요가 없습니다.

좋아요.

음, 그래서 또 다른 재미있는 것을 보여드리겠습니다.

좋아요, not을 다시 정의하고 x라는 값을 지정해 보겠습니다.

아그다에는 구멍이나 목표라고 하는 것이 있습니다.

그래서 물음표를 입력하고 로드하면 옆에 숫자가 있는 멋진 작은 녹색이 나타납니다.

그리고 맨 아래에 타입을 알고 있기 때문에 이 구멍에 부울 타입의 뭔가를 넣을 것으로 예상합니다.

그리고 Ctrl+C, Ctrl+콤마를 누르면 목표와 거기에 도달하기 위해 지금까지 가지고 있는 컨텍스트가 표시됩니다.

그래서 이 경우 부울을 예상합니다.

그래서 이 부울은 결과이고 x라는 부울 타입의 뭔가가 있다고 합니다.

바로 거기에 있습니다.

그리고 정말 재미있습니다.

저는 항상 구멍을 사용합니다.

그리고 연습 문제에도 구멍이 있습니다.

값을 채울 수 있습니다.

그리고 여기에 매개변수의 이름을 입력합니다.

x를 입력하고 Ctrl+C, Ctrl+C를 누르면 k 분할됩니다.

그래서 위에서 정의한 두 가지 경우가 모두 표시됩니다.

탐색하려면 Ctrl+C, Ctrl+F를 누르면 다음 구멍으로 이동합니다.

그래서 앞으로 이동할 수 있고 Ctrl+C, Ctrl+B를 누르면 구멍을 뒤로 이동할 수 있습니다.

그러면 구멍을 탐색할 수 있습니다.

그리고 같은 작업을 수행할 수 있습니다.

뭔가를 입력하면 구멍을 채우고 입력한 내용이 실제로 부울 타입인지 확인할 수 있습니다.

목표와 일치하는지 확인하려면 Ctrl+C, Ctrl+스페이스바를 누르면 채워집니다.

Ctrl+C, Ctrl+F를 눌러 다음 구멍으로 이동하고 이 경우를 거짓으로 지정하고 싶다면 Ctrl+C, Ctrl+스페이스바를 누릅니다.

타입 검사를 통과하지만, 예를 들어 작동하지 않는 뭔가를 입력했다고 가정해 보겠습니다.

xyz와 같이 xyz가 없는데 Ctrl+스페이스바를 누르면 xyz가 무엇인지 모른다고 불평할 것입니다.

좋아요, 이제 두 개의 함수가 있습니다.

음, 더 복잡한 함수를 만들어 보겠습니다.

그래서 and는 음, 두 개의 부울을 입력으로 받습니다.

하지만 아그다에서는 모든 함수가 하나의 매개변수를 받습니다.

그러면 어떻게 할까요? 글쎄, 함수형 프로그래밍에 익숙하다면 커링에 익숙할 것입니다.

그리고 그것은 기본적으로, 여러 매개변수를 가진 함수와 동일한 작업을 시뮬레이션할 수 있습니다.

첫 번째 매개변수를 받아서 하나의 매개변수를 받는 다른 함수를 반환하는 함수를 사용하면 됩니다.

계속 확장할 수 있습니다.

그래서 화살표가 많이 있는 표현식을 볼 때, 기본적으로 이 화살표는 오른쪽으로 결합됩니다.

그래서 이것과 같습니다.

음, 궁금한 사람이 있으면 어떻게 생겼는지 보여드릴 수 있습니다.

그래서 이제 경우 분할을 하면 재미있는 점은 이제 두 개의 매개변수가 있다는 것입니다.

하지만 대부분의 경우 두 개의 인수를 받는다고 가정하고 그냥 읽으면 됩니다.

좋아요, 이것은 하나의 인수를 받고 또 다른 인수를 받습니다.

마지막 것은 부울입니다.

그리고 대부분의 경우 이 작은 워크숍에서도 그렇게 읽을 수 있습니다.

음, 그래서 공백으로 구분하여 두 가지를 모두 입력하고 Ctrl+C, Ctrl+C를 누르면 가능한 모든 경우를 k 분할합니다.

그래서 정말 편리합니다.

왜냐하면 나중에 의존적 타입을 다룰 때 이러한 타입 중 일부는 제약되어 불가능한 경우는 결과에 나타나지 않기 때문입니다.

음, 그래서 두 쪽 중 하나라도 거짓이면 거짓입니다.

그래서 거짓이라고 말할 수 있습니다.

거짓 거짓 거짓.

이 경우는 참입니다.

좋아요, 네.

구멍에 있을 때 Ctrl, 뭔가를 입력하고 Ctrl+C, Ctrl+스페이스바를 누르면 확인하고 괜찮으면 채워줍니다.

메뉴가 있는 것 같습니다.

한번 볼까요.

음, 음, k 분할은 없지만 여기 위에 아그다 메뉴에 경우 분할이 없습니다.

음, 아닌 것 같습니다.

네.

경우 분할을 많이 사용합니다.

정말 편리합니다.

그래서 기억하게 되는 단축키 중 하나입니다.

단축키는 많이 있지만 저는 많이 사용하지 않습니다.

그래서 GitHub 페이지에 제 생각에 가장 많이 사용하는 것들을 요약해 놓았습니다.

그리고 아그다 문서를 보면 전체 목록을 볼 수 있습니다.

꽤 많이 있습니다.

이 시점에서 더 궁금한 점이 있나요? 유일한 것은 아니지만, 가장 많이 사용되는 것 같습니다.

이제 Atom에도 아그다 모드가 있습니다.

사람들이 사용하는 것을 본 적이 있습니다.

음, 저는 직접 사용해 보지는 않았지만요.

뭐라고요? 얇은 것이 좋다고요? 오, Vim도요? 네, Vim도 있습니다.

네.

좋아요.

음, 하지만 커서는 목표가 아닙니다.

네, 때때로, 이렇게 목표가 있고 녹색이지만 다른 곳을 변경하면 다시 로드해야 합니다.

왜냐하면 혼란스러워할 것이기 때문입니다.

그래서 저는 항상 Ctrl+C, Ctrl+L을 누르고 있습니다.

네.

좋아요.

음, 음, 좀 더 전술적인 수준의 것들을 가지고 놀아 보겠습니다.

물론이죠.

한번 볼까요.

짠! 어때요? 음, 좋아요, 아그다, 아그다는 밑줄을 여러 가지 흥미로운 방식으로 사용합니다.

정말 재미있는 것을 보여드리겠습니다.

그래서 하스켈에서 가운데에 and가 있는 false and false와 같은 것을 말하고 싶다면, 운이 없다면 뭔가 이상한 기호를 사용해야 합니다.

뭐, 뭐든지.

음, 하지만 아그다에서는 인수가 들어갈 위치에 밑줄을 넣어 함수 이름을 정의할 수 있습니다.

그래서 왼쪽에 밑줄을 넣고 뭔가가 왼쪽에 들어갈 것으로 예상하고, 뭔가가 오른쪽에 들어갈 것으로 예상합니다.

그리고 이렇게 접두사 형식으로 사용할 수 있습니다.

그래서 이제 이것들은 모두 접두사 형식입니다.

음, 전과 마찬가지로 일반적인 이름으로도 사용할 수 있습니다.

그리고 잘 작동할 것입니다.

하지만 and 함수의 정의에서도 가운데에 and를 넣을 수 있습니다.

잘 작동할지 모르겠네요.

네, 어떤 것은 접두사 형식이고 어떤 것은 중위 연산자입니다.

그래서 여기 가운데에 and를 넣을 수 있습니다.

그리고 정말 재미있습니다.

음, 그래서 연습 문제 중 하나는 or입니다.

제가 연습 문제를 제대로 기억한다면.

그래서 연습 문제 01 부울을 열면, or을 직접 정의할 수 있습니다.

그리고 계속하고 싶다면 nand와 nor를 정의할 수 있습니다.

그리고 제대로 확인해 봐야겠지만, 이렇게 중위 연산자 또는 or을 중위 연산자로 사용하여 k 분할을 하면, 네, 중위 연산자로 유지됩니다.

그래서 편리합니다.

네.

참인 경우가 하나뿐이고 나머지는 모두 거짓인 경우, 세 가지 경우를 통합할 수 있나요? 네, 그렇게 해 보겠습니다.

음, 좋아요.

음, 음, 할 수 있는 일이 몇 가지 있습니다.

그래서 한 가지 방법은, 음, 밑줄을 사용하는 또 다른 방법을 살펴보겠습니다.

밑줄은 거짓입니다.

좋아요, 그렇게 하는 방법입니다.

일종의 포괄적인 방법입니다.

음, 그래서 밑줄은 컨텍스트에 따라 다른 의미를 가지며, 앞으로 더 많은 의미를 알게 되겠지만, 등호 왼쪽의 밑줄은 이 값이 무엇인지 신경 쓰지 않고 어디에도 사용하지 않겠다는 의미입니다.

그래서 거기에 뭔가가 들어가야 하지만 무엇인지는 신경 쓰지 않습니다.

그리고 여기서는 그렇습니다.

글쎄, 그리고 이제 순서가 있습니다.

음, 아그다는 기본적으로 위에서 아래로, 왼쪽에서 오른쪽으로 해석합니다.

그래서 참과 참은 참과 같을 것입니다.

그리고 나머지는 중요하지 않습니다.

하지만 이것을 위에 놓으면 아그다는 불평할 것입니다.

이미 모든 것이 거짓이라고 말했기 때문에 그것을 볼 수도 없을 것이라고 말할 것입니다.

그렇게 하는 방법입니다.

음, 그리고 여기서 정확한 분할이라는 새로운 옵션을 사용하고 싶습니다.

왜냐하면 이것은 일종의 작은 방정식을 만들기 때문입니다.

음, 아그다에 대한 한 가지 사실은 어디에나 적용되는데, 같은 것으로 바꿀 수 있다는 것입니다.

그래서 어디에서나 참을 사용하면 참과 참으로 바꿀 수 있습니다.

하지만 이것은 메타 수준에서만 참입니다.

그래서 모든 음, 여기에 있는 줄들이, 참과 참을 바꿀 수 있다는 직관은 모든 줄이 정의상 같을 경우에만 참입니다.

그리고 아그다가 이것을 나누는 방식은 첫 번째 인수부터 사용해야 합니다.

그래서 이 경우 트리를 만들고 첫 번째 인수에서 분기하는지 두 번째 인수에서 분기하는지 알아내려고 합니다.

그리고 이 정확한 분할은, 음, 함수, 여기서 정의한 동등성이 모두 정의상 같도록 보장할 것입니다.

그래서 코드의 어디에서나 참과 참이 있다면 아그다는 차이를 알지 못할 것입니다.

그래서 음, 어떻게 작동하는지 보여드리겠습니다.

그래서 x와 y가 뭔가와 같다면, 한번 k 분할해 보겠습니다.

둘 다 k 분할해 보겠습니다.

좋아요, 다시 채우고 뒤로 작업해 보겠습니다.

그래서 거짓, 여기는 모두 거짓입니다.

거짓, 이런, 거짓, 참, 좋아요.

그래서 여기서 무슨 일이 일어나고 있는지 살펴보면, 거짓인 경우 모두 패턴을 볼 수 있습니다.

거짓인 경우 모두 결과가 거짓입니다.

그래서 그 경우 두 번째 인수는 실제로 중요하지 않습니다.

이제 여기에 정확한 분할이 있고 밑줄을 사용하고 있지만, 확실히 같다는 것을 보장합니다.

그래서 기본적으로 어딘가에서 거짓과 뭐든지가 있다면 항상 거짓이 될 것입니다.

두 번째 경우에는, 음, 참과 다른 뭔가는 항상 그 다른 뭔가를 돌려준다는 점에 유의하여 단순화할 수 있습니다.

그래서 두 번째 매개변수에 이름을 지정하고 그냥 반환하여 이렇게 단순화할 수 있습니다.

그리고 이것이 단순화하는 한 가지 방법입니다.

구멍을 만들 때 마법을 부리는 것 같습니다.

저도 비슷한 문제가 있는데, 나타나지 않습니다.

그래서 물음표를 입력하고 바로 Ctrl+C, Ctrl+L을 누릅니다.

일반적으로 그렇게 합니다.

그리고 길을 잃을 때마다 Ctrl+G를 누릅니다.

때때로 Ctrl+C, Ctrl+N을 눌러 정규화할 표현식을 만들기 시작했는데 취소하고 싶으면 Ctrl+G를 누릅니다.

그리고 거기에 질문이 있습니다.

제 질문은, 음, 함수 적용이 무엇이고 혼합 함수가 무엇인지 알기 위해 편집기의 구문 강조 표시에 의존하고 있는지, 그리고 and를 인수로 캐스팅하는 방법은 무엇인지 묻는 것입니다.

음, 함수 적용과 이러한 중위 및 혼합 고정을 구별하는 방법 측면에서, 함수 적용은 특정 우선 순위 수준을 가지고 있습니다.

그리고 이것들은, 기본값이 기억나지 않지만 함수 적용이 정말 높다고 생각합니다.

그래서 일반적으로 함수 적용이 다른 것보다 먼저 발생할 것입니다.

하지만 기본적으로 이렇게 인수를 제공할 때, 기본값이 기억나지 않지만 기본값은 우선순위가 더 낮습니다.

그래서 기본적으로 공백으로 구분하면 함수 적용이 먼저 발생할 것입니다.

하지만 설정할 수 있습니다.

즉, 중위 l을 지정할 수 있습니다.

즉, and에 중위를 지정하고 숫자를 지정할 수 있습니다.

6, 7이라고 가정해 보겠습니다.

코드에 구문 강조 표시가 없는데 and가 함수에 인수로 전달되는지 또는 입력으로 사용되는지 어떻게 알 수 있을까요? 네, 컨텍스트를 생각해야 할 것 같습니다.

즉, 모든 고정을 지정할 수 있다는 단점은 원하는 바를 직관적으로 알아야 한다는 것입니다.

음, 예를 들어, 예제 1은 false와, 음, 다른 것, x와 false와 같은 것을 and로 하고 싶을 때입니다.

또는 이것을 f라고 부르겠습니다.

그러면 어떻게 알 수 있을까요? 글쎄, 기본적으로 이것은 f가 함수이면 함수 적용이 될 것입니다.

그래서 이렇게 될 것입니다.

음, 만약, 음, 네.

하지만 즉, 구별할 수 있습니다.

왜냐하면 f를 보고 f의 타입이 무엇인지 확인할 것이기 때문입니다.

그리고 함수이면 아마도 함수 적용이라고 생각할 것입니다.

구문 분석 중에 타입 검사를 하는지는 모르겠습니다.

토큰을 구문 분석하는 동안에요.

네.

그 특정 질문에 대해 생각해 본 적이 없지만, 정말 이상한 경계 사례가 많이 있을 것이라고 생각합니다.

그리고 2.4 뭐든지와 2.5 사이에서 구문 분석 동작을 변경했다고 생각합니다.

그래서, 음, 고정을 지정하여 해결할 수 있을까요? 또는 구매한 연산자에 대해 보존되나요? 아니요, 네, 완전히 그렇게 할 수 있습니다.

여기 예제에서 그렇게 했다고 생각합니다.

중위 and를 지정하고 숫자를 지정합니다.

음, 네, 기본적으로 7은, 기본 함수 적용이 무엇인지 기억나지 않습니다.

99 정도로 정말 높다고 생각합니다.

좋아요.

좋아요.

음, 그리고 or이 있다면, 음, 때로는 모든 고정을 나란히 배치하는 것이 좋습니다.

음, 어떤 것이 더 강하게 결합될지 알 수 있기 때문입니다.

그래서 x 또는 y가 뭐든지와 같다면, 음, 그러면 참과 거짓 또는 참과 같은 표현식이 있으면, and가 더 높기 때문에 먼저 참과 거짓을 계산할 것입니다.

그리고 나중에 or을 계산할 것입니다.

그 경우에는 중요하지 않았을 수도 있습니다.

좋아요, 하나 더 해 보겠습니다.

if와 l을 해 보겠습니다.

밑줄은 원하는 만큼 사용할 수 있습니다.

if then else 밑줄은 세 개의 인수를 받습니다.

지금은 모두 부울이라고 가정해 보겠습니다.

아, 유니코드 부울이 사라졌네요.

부울에서 부울로, 부울에서 부울로라고 생각합니다.

그래서 세 개의 입력을 받습니다.

if some b then x else y.

음, 그리고 b를 경우 분할할 수 있습니다.

그래서 거짓이면 두 번째 것을 반환하고 참이면 첫 번째 것을 반환할 것입니다.

그리고 원한다면 여기에 밑줄을 사용하여 해당 인수를 신경 쓰지 않는다는 것을 나타낼 수 있습니다.

아니요, 음, 포기하려고 한다면, 확실하지 않습니다.

그 질문에는 많은 뉘앙스가 있지만, 일반적으로는 게으릅니다.

함수형 프로그래밍에 대해 격렬한 논쟁을 벌일 수 있다고 생각합니다.

전체 언어에서 게으른 것이 올바른 선택이라는 것을 알게 될 것이라고 생각합니다.

네.

음, 그런 것을 보여주는 작은 슬라이드가 있다고 생각합니다.

전체 함수.

그래서 입력이 있고, 집합이 있고, x에서 y로의 함수가 있다면, 전체 함수는 항상 x의 모든 요소를 처리합니다.

그래서 전체 함수입니다.

출력 집합에서 무슨 일이 일어나는지는 중요하지 않습니다.

일대일 함수도 있습니다.

즉, x의 모든 요소가 y의 정확히 하나의 요소에 매핑됩니다.

음, 이 경우에는 정보를 잃어버립니다.

왜냐하면 x의 모든 요소를 처리하고 있지만, y는 모든 요소를 구별할 수 없기 때문입니다.

그리고 여기 아래에 있는 것은 x의 요소 중 하나를 처리하지 않고 있습니다.

그리고 이것은 전체 함수가 아니며, 아그다는 이것에 대해 불평할 것입니다.

여기서처럼 해당 경우를 처리하지 않고 그냥 빼 버리겠습니다.

불완전한 패턴 매칭이라고 할 것입니다.

그리고 뭔가의 참과가 누락되었습니다.

그래서 기본적으로 함수를 작성할 때 입력 집합의 모든 것을 고려해야 합니다.

그리고 이것은 매우 중요합니다.

왜냐하면 그러한 의미에서 함수는 증명이기 때문입니다.

입력 집합의 모든 것을 고려했다는 증명입니다.

그래서 함수는 실제로 전체성에 대한 증명입니다.

해당 매핑의 전체성에 대한 증명입니다.

네, 모든 함수는, 음, 전체적으로 정의되어야 합니다.

음, 끌 수 있는 옵션이 있다고 생각하지 않습니다.

어떤 옵션은 끌 수 있습니다.

예를 들어 종료 검사와 같은 옵션은 끌 수 있지만, 네.

네, 그리고 온라인에서 그에 대한 재미있는 글을 많이 읽을 수 있습니다.

코너 맥브라이드는 최근에 그것이 좋은 것인지 아닌지에 대해 자신의 블로그에서 좋은 글을 몇 개 썼습니다.

그리고 그 주제에 대해 이야기할 시간이 없다고 생각합니다.

좋아요, 그래서 if then else를 만들었습니다.

그래서 참이면 거짓, 그렇지 않으면 참과 같이 쓸 수 있습니다.

이것은 기본적으로 not과 같습니다.

좋아요, not prime을 쓸 수 있습니다.

if를 사용하여 not을 다시 작성해 보겠습니다.

부울에서, 음, 부울로.

그래서 not prime은 부울을 받으면 x가 참이면 거짓을 반환하고 그렇지 않으면 참을 반환합니다.

그리고 이제 not prime에, 음, 참을 전달하면, 음, 거짓으로 줄어듭니다.

좋아요, 아그다와 유니코드에 대한 재미있는 점은 여기에 온갖 이상한 유니코드 문자를 입력할 수 있다는 것입니다.

즉, 이모티콘 같은 것을 마음대로 붙여 넣을 수 있습니다.

음, 그리고 모두 작동합니다.

정말 대단합니다.

그래서 유일한 단점은 모든 것이 공백으로 구분되어야 한다는 것입니다.

공백으로 구분할 필요가 없는 것은 괄호와 이 중괄호로 묶인 것들뿐입니다.

그래서 특히 쉼표가 있는 함수나 데이터 유형을 정의하면, a, b라고 말하고 싶다면 a, b라고 쓸 것입니다.

그러면 a,가 식별자라고 생각할 것입니다.

실제로 구분해야 합니다.

그래서 그냥 참고하세요.

여기서는 쉼표를 사용하지 않는다고 생각합니다.

좋아요, 그래서 아주 좋습니다.

음, 의존적 타입의 소개로 바로 의존적 타입으로 넘어가겠습니다.

준비되었나요? 좋아요, 이 if를 다형성으로 만드는 방법을 보여드리겠습니다.

아마도 항등 함수도 다형성으로 만들 수 있었을 것입니다.

그것부터 시작해 보겠습니다.

좋아요, 음, 뭔가를 다형성으로 만드는 방법은 추가 매개변수를 전달하는 것입니다.

즉, 사용할 집합입니다.

음, 하지만 이제 좋아요, 집합에서 뭐든지로, 뭐든지로 함수를 만들 수 있습니다.

좋은 일이지만, 해당 집합에 이름을 지정하고 싶습니다.

예를 들어 집합을 x라고 부르겠습니다.

그래서 그렇게 할 수 있습니다.

이름을 지정하면 됩니다.

구문은 이렇게 생겼습니다.

이제 여기와 여기에서 x를 사용할 수 있으며, 이것이 음, 다형성 항등 함수를 만드는 방법입니다.

이제, 음, 추가 매개변수를 제공했으므로 여기에 다른 이름을 지정해야 합니다.

이제 이것은, 그래서 이제 항등 함수는 두 개의 인수를 받습니다.

하나는 집합이고 다른 하나는 첫 번째로 제공한 집합의 요소입니다.

그래서 음, 명명에 대한 참고 사항입니다.

이렇게 이름을 지정하면 해당 이름은, 여기 타입 시그니처의 끝까지, 즉 줄의 끝까지 유효합니다.

왜냐하면 다른 줄에 넣을 수 있고 잘 작동하기 때문입니다.

하지만 여기 아래에 있는 x는 완전히 다른 이름입니다.

이것을 abc라고 부를 수도 있습니다.

참고하세요.

왜 x가 이렇게 많이 나오는지, 왜 사용할 수 없는지.

음, 이 이름은 함수 전체에만 적용되기 때문입니다.

그리고 이것은 우리가 x라고 부를 새로운 이름입니다.

죄송합니다.

좋아요, 그러면 이것을 어떻게 사용할까요? 글쎄, 음, 항등 함수를 사용하고 집합을 전달합니다.

글쎄, 부울을 전달합니다.

그리고 부울 값을 전달합니다.

참.

그리고 이것은 참으로 줄어들 것입니다.

항등 함수에, 다른 집합이 여기 위에 있죠? 항등 함수에 1을 전달하면 유일한 값인 tt를 전달할 수 있고 tt를 반환합니다.

우리가 전달한 값입니다.

음, 좋아요, 글쎄, 동기를 부여하지 않았지만 정말 지칠 것입니다.

즉, 이미 정말 중복된 것처럼 느껴집니다.

그래서 아그다는 어느 정도 추론 기능을 가지고 있습니다.

그래서, 음, 정말 잘 확립된 원칙은 아니지만, 일반적으로 나중에 해당 이름을 사용하면 무슨 말을 하는지 알아낼 수 있습니다.

그래서 이 경우, 음, 암시적 인수입니다.

나중에 제공한 내용을 기반으로 이 인수의 값을 추론하려고 합니다.

그 경우 타입을 지정할 필요가 없습니다.

왜냐하면, 음, 타입을 추론하기 위해 Ctrl+C, Ctrl+D를 눌렀을 때 참을 입력하면, 부울이라는 것을 추론할 수 있기 때문입니다.

그리고 마찬가지로 항등 함수에 참을 전달하면, 참을 전달했고 참이 부울이라는 것을 추론할 수 있기 때문에 x가 부울이라는 것을 알게 됩니다.

그래서 이제 우리는 기본적으로 다형성 버전의 항등 함수를 얻었습니다.

네.

네, 중괄호를 제외하고는 차이가 없습니다.

중괄호는 추론되고 괄호는 항상 수동으로, 음, 전달해야 합니다.

음, 그래서 추론이 실패할 수도 있다는 점을 알아야 합니다.

전혀 일반적이지 않습니다.

그리고 전달하기 시작해야 합니다.

그래서 음, 그렇게 하는 방법은 레코드 구문처럼 생긴 것을 사용하는 것입니다.

그래서 항등 함수라고 쓰고, 글쎄, 먼저 순서대로 있다면 여기에 전달할 수 있습니다.

부울 참을 받습니다.

그래서 인수를 괄호 안에 순서대로 넣습니다.

그리고 이것은 참으로 줄어듭니다.

다른 옵션은 암시적 인수가 많이 있고 Ctrl+C, Ctrl+N을 눌러 표현식 항등 함수를 줄이고 싶을 때, 음, 여기에 이름을 지정했으므로 레코드 구문처럼 사용할 수 있습니다.

x를 부울로 지정합니다.

말씀드렸듯이 중괄호 주변에는 공백이 필요하지 않습니다.

그리고 거짓.

그리고 이것도 작동합니다.

마찬가지로 x를 사용하고 싶다면, 여기 아래에 있는 큰 집합을 사용하고 싶다면 같은 작업을 수행할 수 있습니다.

그래서 여기에서 오른쪽 어딘가에서 원한다면 x를 사용할 수 있습니다.

마찬가지로 암시적 인수가 많이 있으면 다른 이름을 지정할 수 있습니다.

예를 들어 x를 abc라고 부르겠습니다.

그리고 오른쪽에서 abc를 사용할 수 있습니다.

abc.

음, 여기서는 별로 유용하지 않습니다.

그냥 무엇이 있는지 보여드리는 것입니다.

괜찮나요? 음, 네, 어떤 의미에서는 사용하고 있습니다.

입력하고 있지만, Ctrl+C, Ctrl+N을 누르면 아그다에게 표현식을 가능한 한 표준 값으로 줄이라고 요청하는 것입니다.

그리고 아그다는 강하게 정규화되어 있기 때문에 입력하는 모든 항은 항상 궁극적으로 같은 값으로 줄어들 것입니다.

때때로 이 값으로 줄어들고 때때로 다른 값으로 줄어드는 일은 발생하지 않습니다.

항상 같은 값으로 줄어들 것입니다.

하지만 REPL에는 일반적으로 주변에 유지하는 메모리에 뭔가가 있습니다.

예를 들어 여기에 이 변수를 만들었고 이렇게 큰 것입니다.

음, 아그다는 실제로 그런 REPL이 없습니다.

어떤 의미에서는 작성하는 코드가 그런 것과 같지만, 좋아요.

음, 괄호에서 중괄호로 전환했을 때 실제로, 함수 정의에서 추가 증인 매개변수를 지정할 필요가 없어서 그렇게 되었나요? 아니면 실제로 각 호출마다 전달해야 했나요? 네, 전달해야 합니다.

즉, 이 형식이었다면, 네, 모든 곳에 전달해야 합니다.

if를 사용하여 보여드리겠습니다.

음, 이 타입이 모두 부울이 되지 않도록 if를 일반화해 보겠습니다.

그래서 음, 좋아요, 먼저 대문자 x가 집합인 경우부터 시작해 보겠습니다.

그리고 이것은 부울을 반환할 것입니다.

글쎄, 결국에는요.

하지만 첫 번째 매개변수는 부울입니다.

왜냐하면 이것이 우리의 검사이기 때문입니다.

하지만 나머지는 모두 x가 될 것입니다.

그래서 이제 약간의 혼합 고정 문제가 있습니다.

왜냐하면 글쎄, 이 거짓은 실제로 집합이어야 하기 때문입니다.

그래서 할 수 있는 일은, 음, 추가하고 또 다른 것을 추가하는 것입니다.

와! for, 음, x는 myset x입니다.

그래서 이제 우리는 이 for if를 가지고 있습니다.

그래서 이제 글쎄, 이제 두 개의 인수를 받습니다.

하나는 집합이고 다른 하나는, 음, 이제 정말 4, 부울에 대한 4, x이면 거짓, 그렇지 않으면 참입니다.

그리고 부울 타입이 아닌 이 tt를 입력하려고 하면 저에게 소리칠 것입니다.

부울 타입이 아니라고 말입니다.

음, 그런 것입니다.

하지만 즉, 이미 여기에 부울이라고 말했기 때문에 이것들은 부울이라고 추론할 수 있습니다.

정말 중복된 것처럼 느껴집니다.

그리고 이런 식으로 프로그래밍을 더 많이 할수록, 특히 증명을 할 때 정말 지칠 것입니다.

그래서 여기에서 추론한다면, 글쎄, 그러면 여기에 첫 번째 매개변수가 필요하지 않습니다.

음, 안타깝게도 다시 가져오기는 어려울 것입니다.

이렇게 하고 싶다면, 하지만 그러면 전과 같은 상황으로 돌아갑니다.

그래서 x이면 거짓, 그렇지 않으면 참입니다.

그리고 이것을 단위라고 부르고 싶고 1로 두었다면, 글쎄, 별로 유용한 일은 아니지만, 죄송합니다.

괴롭힘.

좋아요.

그래서 아그다의 한 가지 멋진 점은, 즉, 이것은 실제로 의존적 타입의 예입니다.

왜냐하면 여기에서 if를 이렇게 사용하면 x가 부울이라고 가정하기 때문입니다.

하지만 x를 여기 위에 있는 것으로 바꾸면, 글쎄, 여전히 작동합니다.

왜냐하면 여기 위에 정의된 x이기 때문입니다.

하지만 x를 1로 바꾸면 아그다는 불평할 것입니다.

그렇죠? 1이 부울이 아니라고 말입니다.

그래서 이것이 의존적 타입의 한 가지 예입니다.

즉, 함수의 타입, 즉 반환 타입은 이전 인수에 의존합니다.

그래서 여기에서 이 x는 이 x와 같습니다.

그래서 이것이 의존적 타입의 간단한 예입니다.

그래서 이제 이 if는 다형성입니다.

모든 집합에서 작동합니다.

그래서 이것이 다형성입니다.

실제로 의존적 함수입니다.

즉, 여기에서 이 x는 이 x에 의존합니다.

좋아요, 이제 의존적 타입으로 넘어가 보겠습니다.

음, 여러분, 의존적 타입을 사용할 준비가 되었나요? 이 부분이 좀 어렵습니다.

좋아요.

의존적 타입.

그래서 지금까지는 모두 매우 쉽고 익숙했을 것입니다.

하지만 이제 좀 더 어려워질 것입니다.

괜찮나요? 좋아요, 의존적 타입은 기본적으로 값에 대한 타입입니다.

즉, 타입은 값에 의존합니다.

그래서 지금까지는 타입에 대한 값만 다루었습니다.

예를 들어 참은 부울이고 tt는 1입니다.

하지만 이제 우리는, 음, 약간 이상한 표기법을 사용할 것입니다.

하지만 그것은 값을 가진 타입입니다.

좋아요, 그래서 이것이 의존적 타입의 핵심입니다.

그래서 의존적 타입의 한 가지 예는 동등성입니다.

그래서 동등성은 두 값이 같다는 진술입니다.

그래서 동등성을 나타내기 위해 세 개의 막대가 있는 이 유니코드 문자를 사용합니다.

이것이 동등성입니다.

이것을 _≡_라고 입력하면 됩니다.

그러면 동등성을 얻을 수 있습니다.

그리고 두 값을 받습니다.

즉, 첫 번째 값은 집합이고 두 번째 값도 같은 집합에 있습니다.

그리고 결과는 집합입니다.

하지만 여기에서 이 세 번째 집합은 이 두 값에 의존합니다.

즉, 두 값이 같으면 집합에 요소가 하나만 있습니다.

refl입니다.

refl은 reflexivity의 약자입니다.

즉, 모든 것은 자기 자신과 같다는 것입니다.

하지만 두 값이 다르면, 음, 이 집합은 비어 있습니다.

즉, 두 값이 다르다는 것을 증명할 수 있는 방법이 없습니다.

그래서 이것이 의존적 타입의 예입니다.

즉, 결과 타입은 입력 값에 의존합니다.

좋아요, 이제 이것을 사용하여 몇 가지 증명을 해 보겠습니다.

음, 먼저 항등 함수가 자기 자신과 같다는 것을 증명해 보겠습니다.

그래서 identity ≡ identity라고 쓰겠습니다.

그리고 이것이 우리의 목표입니다.

이것을 증명하기 위해 refl을 사용할 것입니다.

왜냐하면 항등 함수는 자기 자신과 같기 때문입니다.

그래서 여기에 refl을 입력하면 증명이 완료됩니다.

좋습니다.

이제 조금 더 복잡한 것을 증명해 보겠습니다.

음, not 함수를 두 번 적용하면 항등 함수가 된다는 것을 증명해 보겠습니다.

그래서 not (not x) ≡ x라고 쓰겠습니다.

그리고 이것이 우리의 목표입니다.

이것을 증명하기 위해 x에 대한 경우 분할을 사용할 것입니다.

그래서 x가 참이면, 음, not (not true)는 not false와 같고, 이것은 참과 같습니다.

그리고 이것은 x와 같습니다.

그래서 이 경우는 증명되었습니다.

이제 x가 거짓이면, 음, not (not false)는 not true와 같고, 이것은 거짓과 같습니다.

그리고 이것은 x와 같습니다.

그래서 이 경우도 증명되었습니다.

그래서 우리는 not 함수를 두 번 적용하면 항등 함수가 된다는 것을 증명했습니다.

좋아요, 이제 좀 더 복잡한 것을 증명해 보겠습니다.

음, and 함수가 교환적이라는 것을 증명해 보겠습니다.

즉, x and y는 y and x와 같습니다.

그래서 x and y ≡ y and x라고 쓰겠습니다.

그리고 이것이 우리의 목표입니다.

이것을 증명하기 위해 x와 y에 대한 경우 분할을 사용할 것입니다.

그래서 x가 참이고 y가 참이면, 음, 참 and 참은 참 and 참과 같습니다.

그래서 이 경우는 증명되었습니다.

이제 x가 참이고 y가 거짓이면, 음, 참 and 거짓은 거짓 and 참과 같습니다.

그래서 이 경우도 증명되었습니다.

이제 x가 거짓이고 y가 참이면, 음, 거짓 and 참은 참 and 거짓과 같습니다.

그래서 이 경우도 증명되었습니다.

이제 x가 거짓이고 y가 거짓이면, 음, 거짓 and 거짓은 거짓 and 거짓과 같습니다.

그래서 이 경우도 증명되었습니다.

그래서 우리는 and 함수가 교환적이라는 것을 증명했습니다.

좋아요, 이것으로 의존적 타입에 대한 소개를 마치겠습니다.

보시다시피 의존적 타입을 사용하면 프로그램의 속성에 대한 증명을 작성할 수 있습니다.

이것은 매우 강력한 기술이며 소프트웨어의 정확성을 보장하는 데 사용할 수 있습니다.

질문이 있나요?

---

Part 1 end. Part 2 Start.

그래서 타입이나 클래스는 액티브의 퍼스트 클래스 객체야.

맞아, 집합과 타입은 모두 그냥 매개변수일 뿐이야. 음, 여러분이 마주치게 되는 차이점은 함수를 정의할 때 이 부분이 집합의 이름이어야 한다는 거야. 생성자가 될 수 없어. 함수 타입 시그니처에 생성자를 넣을 수 없어. 하지만 그 외에는 이렇게 정말 깔끔한 계층 구조를 가지게 돼. 우리는 "타입이 뭐지?" "true의 타입이 뭐지?"라고 묻지. 음, true는 boolean 타입이고, boolean은 집합이거나, 집합이라고 하고, 그럼 "집합의 타입은 뭐지?"라고 묻지. 그건 집합 1이야, 기억나?

그래서 여기서 일어나는 일은 러셀의 역설을 피하기 위해 모든 집합이 일종의 메타 레벨 자연수로 매개변수화되는 거야.

그래서 우리가 집합이라고 할 때 실제로는 집합 0을 의미하는 거야.

음, 집합 0은 다른 집합 0에 대해 이야기할 수 없어. 집합 1의 타입이어야 하고, 그럼 "집합 1의 타입은 뭐지?"라고 묻겠지. 그건 집합 2야. 그리고 "집합 99999의 타입은 뭐지?" 0이 저렇게 많이 있는 거 말이야.

그래서 아그다는, 음, 어쩌면 넣고 싶었을 수도 있어.

음,

어쩌면 이것은 더 이상 소수가 아니야.

하지만 어쩌면 boolean을 넣고 집합을 반환하고 싶을 수도 있어.

그래서 x가 true이면 boolean을 반환하고, 그렇지 않으면 집합 1을 반환하고 싶다고 말하고 싶을 수도 있어.

그럼 거기서 문제가 생길 거야. 왜냐하면 내가 전달하는 이 x는, 아그다가 추론하려고 하는데,

음,

집합을 추론하고 있지만, 집합은 자신에 대해 이야기할 수 없기 때문에 실제로는 집합 1이 되어야 해.

그 경우에는

집합을 인수로 전달하고 있기 때문이야. 그래서

아그다는

레벨을 전달하여 입력 집합을

일반화하거나 추상화할 수 있도록 해.

레벨

그리고 여기에 내장된 것이 있어. 이런, 유니코드가 또 나왔네. "레벨"이라는 내장된 것이 있어.

"레벨"이라는 이름을 얻으려면 모듈을 가져와야 해. open import

primitive

그리고 그걸 사용할 수 있어. 아그다의 모듈에 대한 좋은 점은 어디서나 열 수 있다는 거야. 좋아, 그래서 import agda.primitive는 이제 이 모듈의 모든 것에 액세스할 수 있다는 것을 의미하고, 하지만 그들은 모두 강력하게

정규화되어 있어.

그리고 열면

모든 이름이 최상위 레벨로 던져지기 때문에 "레벨"을 그냥 사용할 수 있어. 그게 아이디어야.

실제로는 사용하지 않았어. 그래서 여기 집합, 이제 정말로 종속 타입을 얻게 되었지.

집합은

여기에 인수를 전달하고 있어.

집합에, 아까 말했던 레벨이야.

음, 이제 내 것이 여기에 있어.

알다시피, 여전히 유효해. 여전히

boolean에서 boolean으로 돌아갈 수 있어.

어, true이고

아니, false. not은 실제로 false야. 그건 true야.

아, true.

그래서 이것은 어디에서나 볼 수 있는 일반적인 패턴이야. 일종의

좋지만,

모든 곳에 유니버스 레벨을 지정하는 것이 정말 피곤해.

다른 시스템은

다른 일을 해.

누펄의 어떤 버전에서, 누펄의 새 버전에서

모든 집합이 유니버스 레벨을 가지고 있다고 가정하고, 주어진 제약 조건을

해결하려고 시도했는지 기억이 안 나.

집합을 전달하면 다른 집합보다 하나 더 큰 집합이 필요하다고 가정하고, 그걸 자동으로 해결하려고 시도해. 반면에 아그다에서는 모두 전달해야 해.

그렇게, 즉 지금은 매우 장황해 보이지만, 다른 이름을 지정할 수 있어. a라든가.

아니면 정말 멋있게 유니코드를 사용하고 싶다면 백슬래시 ell을 입력하면

이렇게 멋진 작은 l 모양을 얻을 수 있어.

음,

어, 그래, 하지만 문제는,

그래, 문제를 보여줄게. 금방 나타날 거야.

좋아, 쉬어야 할까? 꽤 길게 얘기했잖아.

괜찮아?

어쨌든 나는 쉬어야 해. 그냥 계속해.

좋아, 그럼

이제 우리가 일종의

너무 깊이 들어가기 전에, 이 방향으로 조금 더 깊이 들어가서 동등성을 정의해 볼게.

그럼 "동등성"이라는 정의를 소개하자.

좋아, 그럼

음,

음,

이제 우리가 여기서 해온 것은 일종의

어, 슬라이드가 몇 개 있는 것 같아. 그냥 아이디어를 줄게. 와, 정말 작네.

여기에 집합 a에서 집합 b로의 함수가 있으면 첫 번째 함수에 이름을 지정할 수 있어.

왼쪽과 오른쪽에 a, 두 번째 함수의 매개변수야. 우리는 이미 그런 식으로 했지.

맞아, 집합은 실제로 매개변수를 취할 수 있고,

그게 레벨이야.

음,

그래서

이제 "집합 b의 타입은 뭐지?"라는 질문을 해.

집합 b를 보면

인수 a를 취하기 때문에 집합 b는 어떤 것에서 어떤 것으로의

함수가 되어야 해.

좋아,

그럼 왼쪽에서는

타입이, 알다시피, a인 것을 취하는데,

a가 무엇이든, 그리고 a가 무엇인지 알고 있어. 집합 a의 타입이야. 그래서 함수의 왼쪽은 집합 a가 될 거야. 하지만 오른쪽은 뭐지? 기억나? 집합을 정의할 때, 어떤 집합 이름이라고 할 때, 타입이 집합이라고 했어. 그래서

이러한 데이터 타입의

타입은 집합일 뿐이야.

그래서

종속 함수는

궁극적으로 집합에 있는 것에서

또는 원한다면 집합의 어떤 계층 구조에서

어떤 것으로의 함수야. 그래서 우리가 지금 가진 것이 그거야. 그런 집합을 어떻게 만들지? 예를 들어 보여줬는데, 일종의 내장된 것이야. 집합에는 이 내장된 레벨 개념이 있어. 실제 메타 이론처럼

집합은 항상 모든 곳에 이 매개변수를 가지고 있어. 하지만 우리 자신을 위해 어떻게 만들지?

[음악]

그리고 보여줄게. 집합 이름은 집합으로 끝났지만, 집합을, 집합 b를 이름으로 지정할 수 있어. 좋아, 여기에, 음, 집합 타입을 넣을게. 하지만 실제로는 집합 타입이 아니야. 이 함수가 될 거야. 그래서 아그다에서 정의하는 방법은 맨 위 줄에 함수를 넣는 거야. 기억나? 여기 위에서 boolean을 정의해야 했지.

boolean은 집합 타입이라고 하고,

여기 위에는 함수가 전혀 없어.

좋아,

그래서 그게 우리 타입이야.

이제 생성자는, 이 타입 시그니처에 값을 얻는 방법은 몇 가지가 있는데, 그게 무슨 의미인지 좀 혼란스러워.

기억해,

집합 b는 이제 매개변수를 취해야 하기 때문에

기억나? 여기 각 생성자에서

false는 boolean 타입이라고 했고,

true는 boolean 타입이라고 했어.

다시 돌아가서

좋아, 그래서 여기, 음, 이제 집합 b, 집합 b라고 할 수 없어. 왜냐하면 다른 인수를 기대하고 있기 때문이야. 그래서 하나를 줘야 해. 집합 a가 무엇인지 알고 있다면 몇 가지 옵션이 있어. 때로는 하드코딩된 값으로 제한하고 싶을 수도 있어. 이제 집합 b를 보면

음, 매개변수 생성자 a를 제공하지만, 각

생성자도 인수를 취할 수 있고, 그 경우에는

여기 있는 a를 이 집합의 인수로 사용할 수 있어.

그리고 그게 우리가 시작한 방식이야. 기억나? 다른 집합 타입 a가 주어졌을 때

이제 다음 집합은 실제로

우리가 제공한 것보다 그 값에 따라 달라지는

함수를 만들었어.

음, 그래서 그렇게 보여. 그게 꽤 일반적인 시그니처야.

그리고 이것은 하드코딩된 값을 제공하는 다른 경우야. 그래서

생성자 1, 그 경우에는 타입이 어떤 값이라고 말하면

이제 값이지. 일반적으로는

boolean 타입 값이라고 했잖아.

내 bool을 말할 때, 내 bool이 boolean 타입이라고 했고,

특정 값이 무엇인지 물었지. 타입이

boolean인데, 값은 뭐지? 이 경우에는 true야.

이제 타입에는 추가 매개변수가 있어.

음, 집합 b인데,

생성자 a가 값처럼 되어 있어.

이 경우에는 하드코딩했기 때문에 생성자 1은 매개변수를 취하지 않아. 그래서 실제로는

생성자와

어, 1

생성자가 매개변수를 갖는 더 일반적인 경우와 같아. 값을 제공하면 생성자 1은

음,

값을 취해야 해. 그래서 생성자 1은 이제 전달한 값을 취하는데, 이 경우에는 a야. 이제 이것들은 일치해야 해.

타입을 제한했기 때문이야.

여기서 이러한 생성자로 집합 a가 무엇인지 제한했기 때문에

일반적으로

맞아,

그래서

그래,

cstr은 생성자의 약자야. 이것은 a의 생성자야. a가 bool이라면 true일 수 있어.

그런 식으로.

좀 추상적이지만, 음,

그래, 어쨌든,

일반적으로 이런 이름이 많이 떠다니는 경우, 아까 말했듯이 이 이름은 여기까지 유효할 뿐이야.

그래서 이러한 각 줄, 제공하는 모든 이름은 독립적이야.

그리고 모두 균일하다면 상황을 개선할 수 있는 방법이 있어. 하지만 먼저 동등성이 어떻게 생겼는지 보여줄게.

그래서 동등성은, boolean에 대한 동등성만 해보자. 두 boolean이 같다고 말하고 싶어. 그래서

두 boolean을 여기에 넣을게.

여기서 우리가 가지고 있는 직관은

타입이, 이제 증명이라고 할게.

이제 true가 true와 같다는 것을 증명할 거라고 말할 거야. 그리고 그게

타입 뒤에 있는 직관이야. 증명은 여기에 넣을 거야.

음, 이제 비어 있는데,

실제로 증명할 방법이 없어. 하지만 증명할 방법을 알려줄게.

어떤 사람들은 이것을 반사성을 의미하는

러플이라고 불러.

뭐든 간에,

지금은 그냥 같다고 할게.

그래서 같음은, boolean을 전달하면 x라고 부르는데,

우리가 얻을 것은

음, x가 x와 같다는 것을 안다는 거야. 너무 당연하게 들리지.

왜 그렇게 하는지 모르겠지만,

기억나?

아그다 타입 이론에서 같음을 같음으로 대체할 수 있다고 했잖아.

어디서나, 그리고 not false가 true와 같도록 정의했어.

그래서 not not false는 어디에서나 true와 같을 거야. 그래서 실제로 not false라고 할 때 여기 아래에서 할 수 있어. 이제 직관적으로 이해가 되는 진술을 얻었어.

이 타입은 명제야. 타입으로서의 명제에 대해 들어봤을 거야. 이제 만든 타입은 명제와 같아. not false가 실제로

true와 같다고 말하고 있어.

하지만 그 전에,

매우 사소한 경우를 보여줄게. 왜냐하면 그게 우리가 하고 있는 것처럼 보이기 때문이야. 그래서 이제 같음,

같음을 입력하면 매개변수를 하나 취하는데,

음,

방금 한 것처럼, 전체를 채우는 대신

음, Ctrl C Ctrl R을 하면,

R은 정제를 의미하는데, 두 가지 경우에 사용돼. 하나는 생성자와 같은 것을 입력하기 시작했는데 인수가 무엇이 될지 아직 모르는 경우,

그 생성자 이름을 여기에 채워줘. 같음,

그런 다음 나머지 인수에 대한 구멍을 제공해. 인수가 세 개라면 구멍이 세 개 생길 거야.

다른 옵션은

이 문제에 대한 해결책이 하나뿐인 경우 정제가

해결책의 시작을 제공한다는 거야.

그리고 같음 타입의 것을 만드는 방법은 하나뿐이라는 것이 밝혀졌어.

바로 같음이야. 이제 구멍 안에 있을 때 Ctrl C Ctrl 쉼표를 누르면 무엇을 찾고 있는지 알려준다는 것을 기억해.

음, boolean을 찾고 있어.

음,

그래서 이제 이 타입 시그니처는

이 생성자를 사용하면

특정 값의 같음 타입의 것을 만들려고 하는데 false를 전달하고 있기 때문에 작동하지 않을 거라고 말하고 있어.

하지만 여기에 true를 전달하면

만족스러워. 왜냐하면 타입 검사를 할 때 실제로 하는 일은

맞아, 게으른지 아닌지 물었잖아.

이 첫 번째 인수를 취해서

줄이고, 두 번째

인수를 취해서 줄이고,

그런 다음 여기 있는 이 항을 볼 때,

이 값 같음은 이 인수를 취해서

줄이고, "이것들이 모두 같은 값으로 줄었나?"라고 말해. 아그다는 강력하게 정규화되어 있다는 것은

모든 항이 표준 항으로 줄어든다는 것을 의미해. 그래서 줄이면

이 세 개의 표준 항이 모두 같은지, 그리고 그게 여기서 실제로 한 일이야. 그래서 true가 true와 같다는 것을 증명했어. 그다지 흥미롭지는 않지만,

말했듯이 정의적 동등성을 만들었잖아.

맞아,

not false는 true로 정의되어 있어.

따라서 not false도

true로 줄어들 거야.

맞아, 그래서 이제 Ctrl C Ctrl N으로 돌아가서 표현식을 정규화하거나 줄여.

그리고 not false를 입력하면 true로 줄어들어. 이제 왜 그렇게 하고 싶은지, 어디에 맞는지 이해하기 시작했어.

왜냐하면

여기서

음, not false는 true로 줄고, true는 true로 줄고, true는 true로 줄어들어. 그래서 우리는

모든 것이 같은 값으로 줄어드는 진술을 했어.

말했듯이,

n번째 정도까지 가져가면

여기에 not false를 넣으면

타입 검사가 통과해. 왜냐하면 모두 true로 줄어들기 때문이야. 음, 여기에도 not false를 넣을 수 있어.

왜냐하면

모두 같은 값으로 줄어들기 때문이야. 아니면 not,

true를 다시 여기에 넣을 수 있어. 모두 같은 거야.

좀 이상하지만, 이게 정말로,

강력하게 정규화한다는 개념과 생성자가 여기 위에서 일어나는 일을 제한한다는 개념이

일종의 제약 조건을 제공하고,

이제 제약 조건에 대해 이야기할 수 있어. 여러 제약 조건을 만들 수 있고,

음,

문제가 있는데,

자연수를 다룰 때 더 잘 알 수 있을 거야.

몇 가지 더 해보자.

맞아, 더 복잡하게 만들 수 있어. not of not of

true를 하면

결국 같은 것으로 줄어들어. 그리고 여기에 true를 입력하는 것이 지겹네.

그래서 추론할 수 있다고 말했던 것을 기억해.

여기에 두 개의 값을 제공하고 있기 때문에

타입을

추론할 수 있어.

그래서 이제 같음은 더 이상 매개변수가 필요 없어.

하지만 아그다가 혼란스러워하면 생각한 대로 작동하지 않을 거야.

true를 전달할 수 있고,

정말로 필요하다면 x는 true라고 전달할 수 있어.

부분 추론이라는 뜻인가?

그래, 부분 추론이야. 왜냐하면 이론적으로는 이론의 모든 것을 추론할 수 없지만,

일반적인 경우에는

도움이 되도록 노력하고, 때로는 실제로

추론할 수 있는 것에 놀랄 때가 있어. 논문을 읽었는데, "실제로 이 적용적인 것을 추론할 수 있어."라고 말하더라고. "와, 멋지다. 몰랐어."라고 생각했지. 논문을 참조했는데, 아그다에서 특별한 추론을 했다는 것을 보여줬어.

일반적으로 해결할 수 없는 문제이지만,

특정 경우에는 대부분 도움이 되도록 만들 수 있어.

우리가 증명할 수 있는 다른 것은 무엇이 있을까? 아, 맞아, 좋아, 좀 더 재미있는 것을 증명해 보자. 우리는 이 모든 함수를 가지고 있어. 그래서

음,

[음악]

우리가 증명할 수 있는 다른 것은 무엇이 있을까? not not true가 true와 같다는 것을

증명할 수 있고, 그건 꽤 간단해.

and true and true가 true와 같다는 것도

증명할 수 있어.

음,

그리고 보면

이것들은 모두 정의적으로 true야.

왜냐하면 증명하기 위해 아무것도 할 필요가 없었기 때문이야. true와 true를 봤을 뿐이야. 음,

여기 true와 true를 취하면 두 번째 것을 반환하고,

그건 true로 줄어들 거야.

하지만 명확하지 않을 수도 있는 것을 증명해 보자.

not이

not prime과 같다는 것을 증명하자. not prime을

if then else로 정의했고, not을 여기서

간단한 패턴 매칭으로 정의했기 때문에

not이

두 가지가

같은 값을 반환한다는 것을 증명할 수 있어. 그래서

boolean이 주어졌을 때

같음을 보여줄 거야.

not of x가

not prime of x와 같음을 보여줄 거야. 그래서 외연성을 증명하는 거야. 같은 입력이 주어졌을 때 이러한 함수는 같은 출력을 반환해.

어, 그래서

어, 같음, 뭐든 간에, 음,

그래서 여기에 boolean이라는 매개변수가 하나 있고, 이제 볼 수 있어. 음, 같음을 입력하면 되는 거 아닌가? 음,

사실 그렇지 않아. 왜냐하면

여기서 일어나는 일은 줄일 수 없다는 거야.

not을 여기 위에서 정의할 때,

꽤 위에서, 특정 값을 제공했지만, 여기서는 값이 무엇인지 아직 몰라. 그래서 아직 무엇이 될지 몰라. 그리고

마찬가지로 not prime, 일종의

아, 아직 잘 모르겠네.

그래서

해야 할 일은 아그다가 정의적 동등성을 얻을 수 있을 만큼 인수를 분할하는 거야.

그래서

false를 기준으로 케이스를 분할하고, 이제 목표를 보자.

그래서 Ctrl C Ctrl 쉼표를 누르면 일종의

부분적으로 정규화하고, Ctrl U를 누른 다음 Ctrl C

Ctrl 쉼표를 누르면 전혀 정규화되지 않아. 그래서 그대로 보여줄 거야. 그리고 Ctrl U Ctrl U를 누르면,

Ctrl U를 두 번 누른 다음 Ctrl C Ctrl 쉼표를 누르면 최대한 정규화하려고 시도할 거야. 그래서

기본값이 맞는 것 같지 않아.

잊어버릴 때를 제외하고는 간단한 케이스를 사용하지 않아.

하지만 정규화되지 않은 케이스인

Ctrl U Ctrl C Ctrl 쉼표를 사용하면

하려는 일이

왼쪽의 not false와 오른쪽의 not prime of false를 줄이는 것임을 알 수 있을 거야. 하지만 이제 not false의 정의적 동등성을 가지고 있어. true이고, 이제 not prime 또는 false를 보면 정의적 동등성을 가지고 있어.

왜냐하면 이 녀석을 줄일 수 있을 거야.

음, 맞아, 일종의 중첩된 거야. 음, f를 취하지만, 이 if를 호출하고, if에는 false에 대한 케이스가 있어. 두 번째 것을 반환할 거야.

그래서 이것들은 결국 같아질 거야. 그리고 그 말은

문제를 줄였다는 거야. 아그다가

두 항을 같은 값으로

줄일 수 있을 만큼 타입을 줄였어.

두 번째 경우에는

같은 거야. 이제 true 케이스에 있고,

완전히 정규화된

버전을 사용하면 둘 다

false로 줄어드는 것을 알 수 있어. 계속할 수 있어.

그래서 같음을 얻게 되는데, 처음에 이런 증명을 봤을 때, 음, 여기에 같음을 넣고 여기에 같음을 넣으면 증명이 말이 안 된다고 생각했어. 하지만 일종의 직관은

여기 위에서 정의적 동등성을 만들고 있고, 아그다는 이러한 다양한 정의적 동등성을

더 이상 할 수 없을 때까지 실행할 수 있고, 그게 표준 값이야.

하지만 문제는

모든 항이 어떤 것으로 줄어드는 것은 아니라는 거야.

왜냐하면 여기에 다른

매개변수가 있어서 줄일 수 있는 것을 제한하기 때문이야. 하지만 매개변수를 분해하고 개별 케이스를 살펴보면 조각을 연결할 수 있어.

음, 그리고 조각을 연결하는 것이

증명이고, 함수형 프로그래밍과 매우 비슷하다는 것이 밝혀졌어. 왜냐하면 실제로 우리가 한 일은

여기서 값을 반환하는 거야. 이 항은 다른 타입을 가지고 있어. 맞아, 이 항은

기억나? 전체를 봤을 때

타입은 not false가 not false와 같음이었어. 타입에 특정 값이 있어.

음,

맞아, 그래서 and의 다른 점은,

음, boolean에 대한 마지막 증명을 하나 더 하고 마무리할게.

음,

and와 함께, 맞아, and false false,

false와 어떤 것이든

false지, 맞아?

그래서 and false,

음,

boolean이 주어졌을 때,

좋아, 여기 멋진 게 있어.

이것을 읽는 방법은 전체 함수라는 것을 기억해. 그래서 "모든"이라고 말할 수 있어.

모든 boolean x에 대해, 주석 처리할게. 왜냐하면 실제로 입력할 수 있기 때문이야.

"모든"

아그다에 실제로 있는 것이지만, "모든"은

전체성을 도입하지 않아. 아그다 언어에는 전체성이 내장되어 있어. 그래서

맞아, 이제 이것은 말 그대로

이것의 동의어일 뿐이야. 하지만 "모든"이 하는 일은, "모든" 시그니처나 유니코드를 사용하는 경우 백슬래시 a-l-l을 입력하면 멋진 "모든" 모양을 얻을 수 있어.

그것은

타입 추론에 대한 구문 설탕이고, 타입 추론은 여기에 밑줄을 넣으면

일종의

기억나? 밑줄은 다른 위치에서 다른 의미를 가지고 있어.

여기 타입 시그니처에서는 "이 타입을 추론해 줘."라는 뜻이야.

그리고 구멍을 넣을 수도 있다는 것이 밝혀졌어.

그리고 일종의

구멍에 들어가서 Ctrl C Ctrl 같음을 누르면

이 구멍의 제약 조건이 무엇인지 알려주고, 이

구멍이 boolean 타입이 되도록 제한되어 있다는 것을 알 수 있어. 그래서 실제로 해결책은 하나뿐이야. 그래서

추론할 수 있고, 따라서 "모든"을 여기에 넣으면

음,

그것의 동의어일 뿐이야.

그래서 입력하면,

맞아, 여기에 주석을 달자.

그래서

그것의 동의어는 "모든 x"일 뿐이야.

그래서

음,

그래서 "모든 x"라고 말할 수 있지만, "모든"은

보편성을 도입하지 않았어. 아그다의 전체 함수가 전체성을 도입했어.

그래서 "모든 x"라고 말할 수 있고, 아니면 멋지게 만들어서 이렇게 "모든 x"라고 할 수 있지만,

실제로는 어떤 타입의 x에 대해서도 "모든 x"가 아니야.

실제로는 모든 boolean x에 대한 "모든 x"야.

음,

그래서 때로는 사람들이

이렇게 하는 것을 볼 수 있어. 읽기 좋기 때문이야. 모든 boolean x에 대해 x라고 부르는 거지.

하지만 실제로는 타입을 지정하면 의미가 없어.

왜냐하면 동의어이기 때문이야.

하지만 입력을 많이 줄일 수 있어. "모든 x"라고 말할 수 있고,

x의 타입을 추론해 줘.

음, 그리고 x의 값도 추론할 수 있다면, 예를 들어 집합이라든가, 나중에 그 집합을 사용하는 경우 중괄호로 묶으면

x의 타입을 추론하려고 시도하고, x의 값도 추론하려고 시도할 거야. 일종의 이중

추론이야.

하지만

나는 전체

이론을 좋아해. 전체 함수를 좋아하고,

시그니처에

유지하는 것을 좋아해.

좋아, 그럼 음,

x, 그래서 말하고 싶은 것은 x와

어떤 것이든,

false와 x는 false와 같다는 거야.

왜냐하면 그게 and의 속성이기 때문이야. 그래서 이제 이것은 속성과 같아.

x가 주어졌을 때, 나는 이걸 항상 해. x를 입력하고,

해결할 수 있는지 묻는 거야.

해결할 수 있다는 것이 밝혀졌어. "왜 바로 해결할 수 있지?"라고 생각할 수도 있어. 반면에 not not은 케이스를 분할해야 했는데, 왜냐하면 왼쪽에

false, 아니, 왼쪽에 어떤 것이든 false와 같기 때문이야. 그래서 그건 정의적으로 true야.

이제 반대로 해보자.

and false를 해보자. 여기서 타입 이론가들이 고통스러워하는 부분이야.

왜냐하면

해결하기 똑같이 어려워야 하기 때문이야.

그래서 x and false가

false와 같아야 하지.

하지만 정의적으로 증명할 수 없어.

음,

여기에 같음을 입력하면 만족하지 않을 거야. "음, 알아낼 수 없어. 미안."이라고 말할 거야.

그래서

이유는 x를 정의한 방법을 보면

어떤 정의에서도 오른쪽의 값을 보지 않았기 때문이야. 그래서

오른쪽을 보고 "오른쪽에 false를 넣으면 항상

false와 같을 거야."라고 깨달을 수 없어. 정의적으로 true가 아니야.

하지만 케이스를 분할하면

이제 우리가 가진 것은,

보면,

false and false가

false와 같다고 말하고 있어. 좋아, 이제 정의적 부등식을 얻었어.

왜냐하면 여기 위에서 false and 어떤 것은

false이기 때문에 정의적으로 true야. 그래서 같음을

넣을 수 있고, 이 경우에는

true and false가 false라는 것을 알고, 일종의 위로 돌아가면

true and 어떤 것은 어떤 것과 같아. 음, 이 경우에 어떤 것은 false이고,

그것은 false와 같아. 그래서 괜찮아.

그럼 왜

이렇게 말할 수 없지? "this and false는

false와 같다."라고 말하고 싶어.

두 가지 케이스가 필요한 이유는 음, 이것이 이것과 같기 때문이야. 여기서 x를 사용하지 않았어.

맞아, 이유는

여기 있는 이

항이 단일 타입을 가지고 있기 때문이야. 타입은 말 그대로 이거야.

맞아,

false와 알 수 없는 boolean 값은 이 경우에는 정의적으로 항상 false일 거야.

케이스를 분할할 때

이 항의 타입은 달라. 이것들은 같은 같음이 아니야. 여기 있는 같음 항은 다른 타입을 가지고 있고, 그게 케이스 분할이 하는 일이야. 두 가지 타입을

명확히 하는 거야.

맨 위 케이스에서 "타입이 뭐지?"라고 물으면

두 위치 모두에 false가 있다는 것을 알게 돼. 왜냐하면 여기서 분할했기 때문에 이제

이 x가 실제로 false라는 것을 알았어. 그래서 이제 오른쪽의 타입은 여기 위에 있는 것보다 더 구체적인

타입을 가지고 있어.

그리고 그게 요령이야. 그래서 길을 잃으면,

원하는 것을 해결하는 다른

증명을 해결하는 속성이 있다면 그 증명을 사용할 수 있지만,

케이스 분할은

종종 증명을 시작하는 방법이야.

좋아,

거기서 놀 수 있어. 하고 싶다면 꽤 많은 다른 연습 문제가 있어.

예를 들어, if and only if, and, xor를 사용하면

음,

nand와 nor, nand는 not

and이고, 그런 식으로

보여줄 수 있어.

시간이 얼마 남지 않았기 때문에 숫자로 넘어갈게.

꽤 많이 줄었어.

음,

하지만 바라건대,

전달하려고 하는 것은

이러한

동등성이 어디에서 오는지, 타입이 어디에서 다른지에 대한 핵심 이론이야. 나에게는 꽤 미묘한 것이었고, 많은 곳에서 자세히 다루지 않았어.

하지만 이렇게 놀면서 배우는 방식이 좋아. 아, 또 다른 점은

같음 또는 일반적으로 중위 연산자로 사용되기 때문에

두 개의 같음을 사용하는 같음과 같은 것을 할 수 있어.

그리고 그 경우에는

증명이 좀 더 보기 좋아질 거야.

그래서 같음과 같은 것을 말할 수 있어.

하지만 이제 모든 곳에서 그렇게 해야 해.

그래, 그래, 그렇게 할 수 있어. 그렇게 하자. 그래야

다시 하는 데 몇 시간을 쓰지 않아도 돼.

음,

그래서

입력할 필요도 없어. 말 그대로

그것이 그것과 같다고 말할 수 있어.

그리고 여기 같음이 마음에 들지 않으면

음,

타입을 추론할 수 있다면 시그니처를 지정할 필요가 없어. 즉, 이것은 어느 정도

타입이, 알다시피,

기억나? 타입 시그니처의 밑줄은

이 타입에 값이 하나만 있다면 특정 것이 되도록 제한되어 있고,

무엇인지 신경 쓰지 않는다는 뜻이야. 음, 구멍으로 가서 일종의,

음, 집합 1의 것을 기대하고 있다는 것을 알 수 있어. 기억나?

왜냐하면 같음은 궁극적으로 집합이기 때문이야.

궁극적으로. 그래서 이 펑키한 것의 타입은 실제로 더 높은 레벨의 집합이야.

그리고 실제로는 이 특정 타입 시그니처인 boolean에서

boolean에서 집합으로 제한되어 있어.

밑줄은

값 타입을

맞아,

어느 정도까지는 맞아.

음,

어,

더 엄격해야 해. 예를 들어, 여기에 밑줄을 넣을 수는 없어.

하지만

그렇게 할 수 있는 특정 케이스가 있어.

지금 당장은 설명하기 어렵지만,

필드가 없는 빈 레코드가 있다면 그 타입을 추론할 수 있어. 그래서 때로는 유용해. 항이 고유하게 지정되어 있다면,

어, 좋아, 여기서 뭘 하려고 했지?

웁스,

음, 맞아, boolean에서 boolean에서 집합으로.

맞아, 그래서 원한다면 채울 수 있어.

타입을 확인해 봐. 같음은 블라블라블라 타입을 가지고 있고, 우리는 "이 이중 같음은 그 타입을 가지고 있어."라고 말했지. 그리고 보라,

이 표기법이 어디에서 오는지 알 수 있어.

대문자 같음이 의미하는 타입을 읽는 데 도움이 돼.

밑줄 같음 같음 밑줄에 1을 넣을 수 있을까? 아,

음,

아니, 왜냐하면

이것 자체가 집합 1의 타입이기 때문이야.

맞아, 그래서 예상하는 것은, 만약 매개변수로 전달되었다면, 그래. 이것의 타입은 무엇이고 붙여넣으면 그걸 얻게 돼.

그래.

이러한 메타 레벨에서 길을 잃기 쉬워.

그리고 나는 쉽게 길을 잃어. 좋아, 자연수를 조금 가지고 놀아보자. 음,

boolean으로 한 것은

데이터가 꽤 간단하기 때문이야. 그래서

자연수나 뭔가가 있다면,

간단한 경우에는 음, 0은 자연수이고, 일종의 1을 더하면

다음 자연수가 돼.

맞아, 그래서 펑키한 것을 할 수 있어.

음, successor라고 불러. 즉,

다음 숫자와 같아.

등등.

음, 그리고 거의 모든 사람이 하는 첫 번째 일은 덧셈을 정의하는 거야.

그래서 덧셈을 정의할 수 있어.

자연수에서 자연수로

자연수.

그래서 x 더하기 y는 블라블라블라와 같다고 말할 수 있어.

그리고 왼쪽을 기준으로 케이스를 분할하면 and와 같은 문제에 직면하게 돼. 음, 0 더하기 어떤 것은

그것이고, successor

어,

두 개를 더한 successor는,

일종의

1 더하기 x 더하기 y는

1 더하기 x 더하기 y와 같다는 것과 같아.

그게 여기서 일어나는 일이야.

좋아, 그럼 더하기에 대한 것을 증명해 보자. 방금 이걸로 한 것과 같은 증명을 보여줄게.

그리고 같은 종류의

고통을 경험하게 될 거야.

음,

하지만 더 나아질 거야.

그럼 같음을 일반화하자. 지금은 boolean으로 하드코딩되어 있지만,

실제로는 집합을 전달하고 싶어.

집합 x나 뭔가를 전달하고, 여기서 그 집합을 사용할 거야. 여기서도.

음, 이제 좋아, 음,

이게 좀 피곤할 수 있어.

왜냐하면

기억나? 이 x의 범위는 저기까지야.

그래서 이제 해야 할 일은

x, x 집합이 주어지고, 그 x의 타입인 또 다른 암시적 인수가 주어졌을 때, 같음

블라블라블라, 아, 맞아, 하지만 같음은 이제 더 강력한 매개변수를 취하는데,

맞아,

하지만 어쩌면 이걸

그래서 여기서 모든 것을 암시적으로 만들 수 있어.

그러면 같은 것을 얻게 돼.

어,

하지만 x가 모든 곳에서 같을 때 이 시그니처가 정말 장황해져. 그래서 아그다는 왼쪽으로 이동하면

작은 약칭을 제공해.

이제 범위가 달라졌어. 기억나? 여기서 x의 범위는 저기까지였지만,

이제 왼쪽으로 이동하면 범위는 전체 정의의 나머지 부분이야.

그래서 이제 전체에서 x를 사용할 수 있고, 그러면

노력을 덜 수 있어. 맞아, x는 여기서 같고,

x는 여기서 같고,

여기, 음, 그리고 슈퍼 일반화하고 싶다면 기억해.

슈퍼 일반화하자.

모르겠어, a는 레벨이고,

어, 왼쪽에는 화살표를 사용하지 않아.

왜 화살표를 넣지 않았는지 모르겠지만, 실제로는 화살표야.

시그니처는 이전과 정확히 같아. 범위, 이름

범위 지정일 뿐이야. 같음의 타입은 무엇이지?

여전히

x, 여기 화살표를 확인해 봐. x에서 x에서 x에서 집합으로. 같은 거야.

그냥, 모르겠어, 다른 것을 추가하기 시작하면

화살표를 좋아하지 않아. 레벨을 정의할 수 있을까?

아니, 아니, 레벨은

어, 원시적인 것이 아그다 맥스에서 말했듯이, 명령을 하고

뭔가 위에 마우스를 올려놓으면 정의로 이동할 수 있어. Ctrl과 가운데 버튼이나 뭔가 그런 거야.

그것은 가정이고, 실제로는 아그다에 내장된 부분이야. 즉,

정의할 수 없어. 다른 이름을 줄 수는 있어.

그래서

모르겠어, "레벨을

대문자 L로 이름 바꾸기"라고 할 수 있어.

그러면 대문자 L이 되어야 하지만,

그게 할 수 있는 전부야.

어,

봅시다, 음, 좋아, 그럼

내가 어디 있지?

좋아,

그냥 타입을 추론해 줘.

음, 이제

추가 레벨을 전달하면

그 타입이어야 해.

미안, 레벨을 사용해야 해.

그래서, 이것은 매우 일반적인 패턴이야. 어디에서나 볼 수 있어. 표준 라이브러리를 열고 아그다 코드를 보면,

주어진, 음, 매개변수가 여러 개라면 abc라고 할 수 있어. 아니면 모두 레벨이라고 할 수 있지만, 문제는 ab 레벨이 있다면

이제 다른 집합 y를

집합 b라고 하고 싶다면 분리해야 해. 그래서 레벨이 세 개라면

여기에 z를 추가해야 하고, 정말 장황해져.

그리고

어쨌든,

다시 돌아가서,

좋아, 그럼 이제 모든 집합을 취하는 같음을 얻었어.

기존 코드는 여전히 작동해. 성공적으로 추상화했어. 그래서

0 더하기

x를 해보자.

모든 자연수가 주어졌을 때

음,

0 더하기 x가

x와 같음을

보여주고 싶어.

누가

음, 맞아, 좋아, 그럼 0,

아그다는 몇 가지 다른 종류의

내장 마법을 가지고 있어.

이

작은 구문을 사용하면

숫자를 정의할 때 기본적으로

자연수에 대한 내장된 것이 내가 여기서 정의한 내 자연수라고 말하는 거야.

그러면 어디서나 십진수 표기법을 사용할 수 있어.

그래서 5를 입력할 수 있고, 5는 실제로 successor

알다시피, 5는

실제로 successor successor successor이고, 5개의

successor가 있어야 해.

맞아, 하지만 5 프라임은 그 구문을 사용하면 5를 입력할 수 있어.

좋아, 그리고 5가 5 프라임과 같다는 증명을

하고 싶을 수도 있어.

그래서 5가 5 프라임과 같다고 말할 수 있어.

제정신인지 확인하기 위해서.

그리고 true야. 같은 거야.

같은 값으로 줄어들어. 이것은 말 그대로 저것에 대한 구문 설탕일 뿐이야.

좋아, 그럼 이 경우에는

음,

정제를 하면, Ctrl C Ctrl R을 누르면 해결책은 하나뿐이야. 0 더하기 x는

정의적으로

x와 같아. 왜냐하면 그렇게 정의했기 때문이야.

0 더하기 어떤 것은 그 어떤 것과 같아. 그게 그냥 그런 거야.

하지만 불행히도 일종의

편을 들어야 해.

이제 x 더하기 0은 그렇게 쉽지 않을 거야. 사실

여기 위에 있는 것보다

훨씬 더 어려워.

좋아, 그럼

구멍에 들어가서

Ctrl C Ctrl R을 누르면

도입 형식을 찾을 수 없어. 즉, 실제로 해결할 수 없다는 뜻이야.

좀 더 크게 말해줄 수 있을까? 잘 못 들었어.

그래,

이거,

그래, 위에서 이중 같음을

같음과 같도록 정의했어. 여기.

내 연산자야. 내장된 것은 없어.

내장된 것은

없어.

다른 코드나 뭔가를 가져오면

하지만 기본적으로, 생각해 보면, 괄호와 이러한

키워드, 데이터와 위치와 같은 키워드를 얻게 돼.

[음악]

기본적으로 얻는 기호는 많지 않아. 즉, "모든",

하지만 공백으로 구분하지 않으면

알다시피, 만들 수 있어. "모든"을 거기에 넣을 수 있어.

그러면

대부분의 것은 공백으로 구분해야 해.

좋아, 그럼 and와 마찬가지로 x를 기준으로 케이스를 분할하자. 이제 타입을 보면, Ctrl U Ctrl C Ctrl 쉼표를 누르면,

u는 정규화하지 말라는 뜻이고,

uu는 완전히 정규화하라는 뜻이고, 아무것도 없으면 그 중간 어딘가라는 뜻인데, 왜 그런지 모르겠어.

음, 그래서 0 더하기 0은 0과 같아.

하지만 완전히 정규화하면

이런, 같은 값으로 정규화되었네. 그래서 괜찮아. Ctrl C Ctrl R을 누르면 고유한 해결책이 하나 있고, 작동해. 이제 이 케이스, 좋아, 약간 문제가 있어. 그래서

정규화되지 않은 것을 보면 successor

x 더하기 0은,

기억해, 함수 적용이 처음에는 더 엄격하게 바인딩돼.

맞아, 그래서 이것은

괄호, 강조 표시된 것과 함께 괄호를 묶고 0을 더하는 것과 반대로,

그렇게 하는 거야.

음, 완전히 정규화하면

그만, 멈춰. 잘못된 위치에 있네.

좋아,

이 녀석처럼,

진짜,

맞아, 레벨이 필요하고, 이제 이 집합 x는 특정 레벨의 집합이고,

x와 0, x가 필요하고, 이제 필요한 것은

마지막 집합이 그 레벨과 같은 레벨을 가지고 있다는 거야.

그게 다야.

그래,

꽤 추상적이야. 음, 이것은 동등성의 내장 정의이고, 실제로 우리는 그것이 필요할 거야.

지금 바로 가져올게.

그래서 이것은 완전히

일반화된 동등성이고, 지금 보여줄 이 멋진 것에 대한 내장 동등성이 있어.

그것을 같음이라고 부르는데,

이것이 저것과 다르기 때문에 문제가 될까 봐 걱정돼.

좋아, 그럼

완전히 정규화하면

음, x 0의 successor가

x의 successor와 같다는 것을 알 수 있어.

그래서 줄어들지 않아.

그래서

아까 지정한 일반 원칙을 기억해. 아그다에서 동등성이 있다면

음,

어디서나 같음을 같음으로 대체할 수 있어. 이제 정의적 동등성은 문제없이 어디서나 대체할 수 있어. 사실 알아차리지도 못할 거야. 아그다는

필요할 때 표준 형식이 무엇인지 알기 위해 줄일 거고,

정의적 동등성은 모두 사라질 거야.

하지만 여전히 액티브

이론은

명제적 동등성을 존중해. 여기서 지정한 것처럼 5는 5와 같아. 그래서 이제

교환할 수 있지만, 문제는

증명을 가지고 다녀야 하고,

이론은 같음을 같음으로 교환하는 것을 존중하지만, 모든 곳에서 그렇게 할 수는 없어.

음,

그리고 여기서 해야 할 일은 다시 쓰기를 사용하는 거야. 그래서

할 일은 음,

x 더하기

음,

0

을

다시 쓰는 거야.

그리고 줄었어. 좋아, 그 전에, 기억해, x 더하기 0은 여기 있는 거야.

그래서 내가 한 일은

어, x, 그래서 x의 타입을 물으면

바로 여기서는 할 수 없어.

그래서 이것이 있었어.

맞아, x 더하기 0의 successor가

여기 x의 successor와 같았어. 이제 재귀적으로 이 함수를 호출하면 증명을 얻을 수 있어.

덧셈을 위해 더하기를 재귀적으로 호출한 것처럼, 이것을

재귀적으로 호출하면

더 작은 x를 사용해서 x 더하기 0이 x와 같다는 증명을 얻을 수 있어.

그리고 다시 쓰기의 아이디어는

증명이 있다면

어떤 표현식에서든

왼쪽을

오른쪽으로 바꿀 수 있다는 거야.

그래서 완전히 줄이면 왼쪽에 x 0이 있고,

왼쪽을 x로 바꾸고 싶어.

그래서 여기서 다시 쓰기를 말할 때,

맞아,

다시 쓰기 p라고 하고,

p가 그것과 같다고 말하고,

다시 할 수 없게 하네.

맞아,

하지만 여기서 아이디어는, 슬라이드를 보여줄게. 어젯밤에 슬라이드를 만들었는데 좀 거칠어.

하지만 아이디어는 왼쪽이 오른쪽과 같다는 동등성 증명이 있다면

왼쪽이 보이는 곳마다

오른쪽으로 바꿀 수 있다는 거야. 그래서 실제로 우리가 한 일은

이제 왼쪽,

x 더하기 0의 successor였던 것을

같음인 x로 바꿨고, 이제 증명이

줄었어. 이제 같다는 사실을 알 수 있어.

그래서 그게 하는 방법 중 하나야. 다시 쓰기는 일종의

슈퍼 레벨 구조물이라는 것이 밝혀졌어.

with 표현식을 사용해서도 할 수 있어.

[음악]

그리고 합동을 사용해서도 할 수 있어. 합동을 보여주고 싶은데, 합동이

동등성에 대한

내가 가장 좋아하는 것 중 하나라고 생각하기 때문이야.

미안, 질문이 하나 있어.

3251이라고 말하고 있는데,

내장된 문이 필요해.

그래, 만약 이 두 녀석을

넣지 않았다면, 그래, 두 번째 것이 없었어. 좋아, 왠지 모르겠지만 이것은 타입을 별도로 제공해야 하고, 값은

자연수를 사용하는 경우, 아, 그렇게 말했지. 일반적으로 소문자 같음이라고 불러.

그래,

그래서 러플이라고 부른다면 일반적으로 러플이라고 불러.

반사성을 의미해.

그래, 그래서 다시 쓰기는

내장된 것, 내장된 동등성으로 정의된 것을 사용해야 해.

음, with 표현식을 사용했다면

간단히 보여줄게.

5분밖에 남지 않았지만,

with 표현식의 아이디어는

일종의

함수 적용이나

표현식의 결과를 아래에서 사용할 수 있다는 거야. 그래서 일종의

추가하는 것과 같아.

음,

이 점 세 개는 이것의 구문 약자일 뿐이야.

그것의 약자.

그래서 음, 일종의

추가 매개변수를 추가하는 것과 같아. 이제 컨텍스트에 이것이 생겼어. 왜냐하면 일종의

호출했거나, 이 함수를 적용해서 결과를 얻었기 때문이야.

x 더하기 0은 x와 같아. 문제는

with가 실제로는

핵심 언어의 일부가 아니라는 거야.

실제로 핵심 언어에서 보조 함수로 구현돼. 간단히 보여줄 수 있지만, 추가

매개변수를 추가하면 이러한 추가 막대를 추가하면 돼.

그래서 r1과 r2가 생겨.

그래서 이제 여기서 무슨 일이 일어나는지 보면,

두 개의 매개변수, 두 개의 자연수를 가지고 있고, x 더하기 0을

일반화했고, 이 증명으로

r1이

x와 같다는 것을 알았어. 그래서 이제 음,

완전히 정규화하면 r1이 x와 같다는 증명을 얻게 되고, 패턴 매칭을 하면, 좋아, 여기 멋진 게 있어.

이 점

구문은

이 값이 특정 표현식이 되도록 제한되어 있다는 것을 의미해. 왜냐하면 동등성,

동등성을 정의한 방식을 기억해.

이 두 가지가

같은 것이 되도록 제한하고 있어. 그래서 패턴 매칭을 하기 전에,

같음을 기준으로 패턴 매칭을 하기 전에,

이것을

x2라고 부르고, 이것을 p라고 부르자. 어때?

그래서 p는 x2와 x가 같다는 증명이고, p를 기준으로 패턴 매칭을 하면

같을 수 있는 유일한 방법은

두 번째 것이 실제로 x인 경우야. 그래서 점은

알다시피, 여기에 밑줄을 사용할 수도 있어. 값이 무엇인지 신경 쓰지 않는다는 뜻이야. 하지만 점을 사용하면

이 표현식이 되도록 제한되어야 한다는 것을 말하는 거야. 그리고 실제로는 어떤 표현식이든 될 수 있어.

왜냐하면 타입을 정의할 때

함수를 전달할 수도 있기 때문이야.

그래서 x가 같도록 제한되면

이제 x의 successor가 x의 successor와 같다는 것을 알고, 그래서 증명이 해결되었어.

그래서 그게 또 다른 방법이야.

그리고 아까 말했듯이,

이것은 실제로 보조 함수를 사용하여 구현돼. 그래서 이전에 x2가 있었고,

x가 있었어.

또는 p나 뭔가가.

그래서 이것의 타입을 보면

우리의 목표는 실제로 함수를 만드는 거야.

그래서 여기에 함수가 있어.

x 더하기 0 aux는

타입이 저것으로 끝나고,

이러한 세 개의 매개변수를 취해.

음,

x를 취하고,

x2는 자연수이고,

증명 p는, 음, 여기서는 p가 필요하지 않지만,

x2가

x와 같다는 것을 알아.

그래서 여기 녀석을 채우면,

x 더하기 0 aux, x를 전달하고,

기억해, 이름을 지정하면

범위는 저기까지야.

그리고 이 증명 p를 가지고 있어. 여기 위에 있는 것과 여기 아래에 있는 것이 매우 비슷해 보이는데, with 표현식을 사용할 때 이면에서 하는 일이기 때문이야. 음, 그리고 일치하면, 즉, 이것은 말 그대로 하는 일이야. 이 보조

함수를 만들고,

이제 같음을

해결할 수 있어. 그리고 이것을 하는 대신,

여기에 주석 처리할게. 그래야

여전히 볼 수 있어.

실제로 x 더하기 0

successor x

는

내가 뭘 했지?

음, 구멍이나 뭔가를 추가해야 해.

음,

x 더하기 0

aux를 호출하면 매개변수를 세 개 취해. 그래서 x를 전달하고,

음,

x 더하기 0을 전달하고,

기억해, 이 함수를 재귀적으로 호출하면

x를 사용해서 x 더하기 0이 x와 같다는 증명을 반환할 거야.

그럼 해결해 보자.

그리고 그게

여기서 with가 하는 일이야. 이면에서 일종의 추가 매개변수를 추가할 수 있도록 해.

결과에 따라 제한될 수 있는

매개변수를.

그리고 명확히 하자면,

두 번째 x는 첫 번째 x와 같은 값이라는 것을 말하는 거야.

음, 이 경우에는 여기 표현식이 x이기 때문이야. 하지만

다른 곳에 y가 있다면 점은

그것이 무엇이든, 괄호를 묶어서, 여기 표현식이 무엇이든

다른 것에 의해 제한된다는 것을 말하는 거야.

제약 조건이라고 기억이 안 나.

하지만

두 개의 자연수가 있고 같다는 증명이 있다면 같을 수 있는 유일한 방법은 같은 값으로 줄어드는 경우야. 그래서

이런 식으로 패턴 매칭에서도 결과를 볼 수 있고,

구문적으로 그렇게 보여.

여기에 x라고 말하면

만족하지 않을 거야. 왜냐하면 "음, 같은 변수 이름을 반복하려고 하네."라고 생각하기 때문이야. 반면에 점을 사용하면 제한된다는 것을 말하는 거고, 이제 이것은

이름이 아니라 실제로는 여기서 오는

표현식이야.

좋아, 그래,

아니, 같음 생성자를 정의할 때 필요하지 않았어. 한 일은

같은 것을 사용한 것뿐이야.

그래서 그게 그렇게 된 이유야. "이 두 번째 것은 이것과 같아야 해."

그래, 불행히도 점은 패턴 매칭에서만 사용돼.

하지만 그래, 이론적으로는 x와 y라고 말할 수 있지만,

문제는 여기서 y를 어떻게 말할 거냐는 거야.

일종의

"y는 실제로 x야."라고 말해야 하지만,

매개변수를 하나만 제공하면

같아지고,

타입 시그니처에 두 개의

매개변수가 들어가. 그래서

5가 6과 같다는 것을

5가 6과 같다고 말해서

표현할 수 있지만, 문제는 음,

어떻게

타입으로 표현할 수는 있지만,

마지막으로, 1분 초과되었지만, 부정의 증명을 빠르게 공유하고 싶어.

음,

이런 문을 증명할 수는 없지만, 거짓이라는 것을 증명하려면

그것에서 빈 집합으로의 함수를 정의하면 돼. 그리고 그것은 5가 6과 같지 않다는 말과 같아.

그래서 부정의 아이디어는,

맞아,

맞아, 그래, 왼쪽이

비어 있다면 오른쪽을 어떻게 매핑할 거야?

비어 있지 않은 집합의 모든 것을 비어 있는 집합으로 매핑할 수는 없어. 그래서 기본적으로 왼쪽이 비어 있다고 아그다를 설득해야 해. 이 경우에는 바로 알아낼 거야.

함수이기 때문에 실제로는 같음 p나 e이고,

패턴 매칭을 하면 아그다, "이것은 불가능해."라는 구문이야.

그리고 음,

불행히도 시간이 부족했지만,

때로는 아그다를 설득할 수 없어. 그래서 아그다가

정의적으로, 실제로 일어나는 일은

어떤 표현식을 줄이고, "음, x는

어떤 경우에는 실제로 어떤 것의 successor와 같아야 해."라고 말하는 거야. 다른 경우에는

실제로 0과 같아야 한다는 것을 알게 돼. 그래서 이제

생성자, 아그다가

같은 것이 하나의 생성자여야 하고 같은 것이 별도의 생성자여야 하는 제약 조건을 찾으면 모순이고,

그러면 음,

여기서 일어나는 일은 아그다가

줄이고 그런 경우를 찾아서 빈 집합으로 매핑할 수 있도록 하는 거야. 그래서 하위 구조는 서로소 범위를 가져야 해.

그럴 필요는 없지만,

음,

변수가

두 개의 별도의 것으로 제한되면 모순으로 간주될 거야. 맞아, 그래서

추가 같음을 여기에 추가하고 같음 프라임이라고 부를 수 있어.

맞아,

작동하지 않을 거고, 파일의 나머지 부분이 만족하지 않겠지만,

그런 타입을 만들 수 있어.

하지만 어떤 이유로든

아그다가 이런 것을 줄이면서

왼쪽에 같음이 하나 있고 오른쪽에 같음 프라임이 하나 있으면 모순으로 간주할 거야.

왜냐하면 제한하고 있고,

다른

경로로 끝날 수 있기 때문이야. 그런 일이 일어날지 모르겠지만,

모델에 이상한 점이 있다는 것을 나타낼 거야. 모순이 되는 것을 원하지 않는다면

문제가 될 수 있어. 하지만 작거나 같음 관계와 같은 경우에는

뒤집어도 괜찮아. 왜냐하면

때로는 x가 y보다 작거나 같고 y가 x보다 작거나 같은 것이 사실이기 때문이야. 사실 그 경우에는

x와 y가 같다는 것을 증명할 수 있어.

자연수로서.

좋아, 시간이 초과되었어. 정말 고마워.

[음악]