[하스켈] GADT(Generalized Algebraic Data Type) 사용하기 (1)

redneval의 이미지

1. 서문

(1) 라이센스 및 저작권

본 문서는 GNU Free Document License 로 배포되므로 자유롭게 수정 및 재배포할 수 있습니다.

단, GFDL 제 4조 D항과 E항에 의해 다음 저작권 표시를 반드시 포함해야 합니다.

---------------------------------------------------------------------------------------------------
Copyright (c) redneval@kldp.org, 2009.
GNU 자유 문서 라이선스 1.3판 또는 자유 소프트웨어 재단에서 발행한 이후 판의 규정에 따라,
본 문서를 복제하거나 개작 및배포할 수 있습니다.
본 문서에는 변경불가부분과 앞 표지구절 및 뒷 표지구절이 없습니다.
Permission is granted to copy, distribute and/or modify this document
under the terms of the GNU Free Documentation License,
Version 1.3 or any later version published by the Free Software Foundation;
with no Invariant Sections, no Front-Cover Texts and no Back-Cover Texts.
---------------------------------------------------------------------------------------------------

(2) 글의 목적

본 문서는 하스켈의 기능 중 하나인 GADT(Generalized Algebraic Data Type) 에 대한 내용을 담고 있습니다.

번역한다면 `일반화된 대수적 자료형'정도가 되겠지만, 본 글에서는 그냥 GADT 라고 하겠습니다.

하스켈 위키에 GADT 에 대한 간략한 설명이 나와있지만 (http://www.haskell.org/haskellwiki/GADT) 설명과 예제가 약간 부족합니다.

(3) 필요 지식

본 문서의 내용을 정확하게 이해하기 위해서는 하스켈에 대한 기본 지식이 필요합니다.

영어로 된 온라인 문서로는 위키책(wikibook ; http://en.wikibooks.org/wiki/Haskell)이 기본기 익히기에는 최고라고 생각하고,

http://book.realworldhaskell.org/read/ 도 추천합니다.

한글로 된 온라인 문서로는 다음 링크를 참조하시고,

http://haskell.springnote.com/

http://wiki.kldp.org/wiki.php/YetAnotherHaskellTutorial

한글로 된 책은 아직 없지만,

입문서인 Programming in Haskell 이 번역되어 곧 출간된다고 합니다. (http://kldp.org/node/98953#comment-484778)

(4) GHC 준비

하스켈을 배우기 위해서는 ghc (Glasgow Haskell Compiler) 가 거의 필수적입니다.

http://www.haskell.org/ghc/ 에서 설치프로그램을 받을 수도 있고

리눅스 사용자라면, 많은 배포판에서 패키지설치를 지원하므로 찾아보시기 바랍니다.

참고로, 우분투에서는 다음과 같이 설치할 수 있습니다.

apt-get install ghc6



2. ADT(Algebraic Data Type)

GADT(Generalized Algebraic Data Type; 일반화된 대수적 자료형) 을 알아보기전에,

먼저 ADT(Algebraic Data Type; 대수적 자료형) 에 대해서 살펴봅시다.

(ADT 는 주로 Abstract data type 의 약자를 나타내며, 본 문서는 설명의 편의상 Algebraic Data Type 의 약자로 사용하고 있습니다.)

ADT 는 다시 구체적 자료형(Concrete data type)과 추상적 자료형(Abstract data type)의 두가지로 나눌 수 있습니다.

구체적 자료형은 Bool, String, [(Int, Int)] 처럼 구체적으로 나타낸 반면에

추상적 자료형은 Maybe a 처럼 a 에 어떤 자료형을 지정하느냐에 따라서 Maybe Int 나 Maybe String 같은 구체적 자료형이 되기도 합니다.

추상적 자료형을 정의하는 예를 살펴보면 다음과 같습니다.

data Maybe a = Just a | Nothing
 
data Tree a = Branch (Tree a) (Tree a) | Leaf a

Tree a 를 살펴보면, Tree a 는 자료형을 나타내고, Branch 와 Leaf 라는 생성자를 정의하고 있습니다.

재귀적으로 자료형을 정의할 수 있고 생성자를 여러개로 정할 수 있다라는 점만 기억하면, 쉽게 사용할 수 있습니다.



3. GADT

이제 GADT 을 살펴보면서, ADT 의 어떠한 제한들이 사라졌는지를 알아봅시다.

(참고 : GADT 를 사용하기 위해서는 ghc 실행시 -fglasgow-exts 옵션이 필요합니다.)

(1) 차이점 : 생성자의 자료형

-- ADT 문법 (컴파일 오류 발생)
data ABC x = A a | B (a -> b)

ADT 방식에서 보면 a, b 는 무엇인지 전혀 알 수 없기 때문에 오류가 발생됩니다.

그렇기 때문에 다음과 같이, 생성자의 인자는 자료형이 명확히 지정돼야 합니다.

-- ADT 문법
data ABC x = A x | B (x -> x)

반면에 GADT 에서는 a, b 가 무엇인지 신경쓰지 않습니다.

-- GADT 문법
data ABC x where
    A :: ABC a
    B :: ABC (a -> b)
    C :: a -> ABC a
    D :: (a -> b) -> ABC (a -> b)

(2) 의문점 : 연산자처럼 생긴 생성자

다음과 같이 코드를 작성하여 gadt.hs 로 저장하고

-- gadt.hs 로 저장함.
module GADT where
data AB x where
    A :: AB a
    B :: AB b
    (:+) :: AB a -> AB b -> AB (a -> b)
infixl 6 :+

(A :+ B) 의 자료형을 한 번 살펴봅시다.

ghci -fglasgow-exts 로 실행을 하고, 다음과 같이 따라하면 됩니다.

Prelude> :l gadt.hs
[1 of 1] Compiling GADT             ( gadt.hs, interpreted )
Ok, modules loaded: GADT.
*GADT> :t (A :+ B)
(A :+ B) :: forall e f. AB (a -> b)
*GADT> 

놀라운 점은, (:+) 연산자의 정의(definition)가 없었는데도 오류가 없다는 것과,

그럼에도 (A :+ B) 의 자료형을 AB (a -> b) 로 정확히 인식한다는 점입니다.

하스켈은 자료형에 대해서는 매우 까다롭게 구는 점을 감안해볼때,

GADT 의 연산자가 정의가 없는데도 무사통과시켜버리는 것은 굉장히 놀라운 일입니다.

하지만 이는 잘못 생각한 것이며, 사실 (:+) 는 생성자입니다.

(:+) 은 생성자이므로, 반환형(return type)은 AB x 형태의 자료형이 돼야합니다.

다음과 같이, 반환형이 AB x 가 아니라면 오류가 발생합니다.

-- (컴파일 오류 발생)
module GADT where
data AB x where
    A :: AB a
    (:+) :: AB a -> a
infixl 6 :+

(3) 공통점

((A :+ B) :+ B) 의 자료형도 알아봅시다.

*GADT> :t ((A :+ B) :+ B)
((A :+ B) :+ B) :: forall a b b1. AB ((a -> b) -> b1)

자, 무슨 일이 일어났는지 살펴봅시다. 설명의 편의상 (A :+ B) 를 X 로 치환해서 설명하겠습니다.

X 의 자료형이 AB (a -> b) 이라는 것은 위에서 이미 언급하였고,

(:+) 의 형(type)은 AB a' -> AB b' -> AB (a' -> b') 로 선언됐으므로,

(X :+ B) 에서 (:+) 의 형은 AB (a -> b) -> AB b' -> AB ((a -> b) -> b') 가 됩니다. (a' 를 (a -> b) 로 바꾸면 됩니다.)

그러므로 (X :+ B) 의 자료형은 AB ((a -> b) -> b') 가 됩니다.

중요한 점은 AB x 라고 하면 x 에는 어떠한 형(type)도 올 수 있다는 점입니다.

x 가 무엇이냐에 따라서 AB (a -> b -> c) 나 AB ((AB a) -> b) 가 될 수도 있다는 점입니다.

이러한 점은 ADT 에도 마찬가지로 적용됩니다.

(4) 자료형(data type)과 형(type)

이 부분은 매우 중요한 내용이므로, 주의해서 읽어주시기 바랍니다.

형(type)은 일반적인 람다 표현식을 말합니다. 예를 들면, x -> y -> z 과 같은 것들 말입니다.

형 중에서 함수가 아닌 것들을 자료형(data type)이라고 부릅니다.

쉽게 말해서 -> 가 하나도 없이 단일한(single) 자료를 나타내는 형이 자료형입니다.

자료형을 세부적으로 분류하면, 기본 자료형(primitive data type)과 ADT(Algebraic Data Type) 등이 있습니다.

(자세한 내용은, http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType)

그리고 ADT 구문에서, 예를 들면 다음과 같은 코드에서

data ABC x = A x | B (x -> x)

x 를 형 변수(type variable) 라고 부르며, 형 변수는 어떠한 형으로던 치환이 가능합니다.

형 변수도 일종의 형(type)이라고 할 수 있기는 하지만,

형 변수의 개념를 명확히 하여, 형이나 자료형과 잘 구분해야합니다.

(5) 요약정리

이제 위에서 설명한 내용을 정리해봅시다.

1) ADT 와 GADT 를 정의하는 구문 안에서는, 형 변수를 사용할 수 있다.
 
2) GADT 구문내에서 연산자처럼 보이는 것은 사실 생성자이고, 생성자이므로 따로 정의를 하지 않고 사용하게 된다.
 
3) GADT 구문내에서 형 변수의 사용이 자유롭다.



4. 예제 1 : SKI 연산

여기부터는, 이 글을 읽는 분들이 GADT 를 제외하고 하스켈에 대해서 어느 정도 알고 있는 가정하에 설명을 계속하겠습니다.

(1) SKI 연산

SKI 연산에는 다음과 같은 규칙이 있습니다.

Sxyz → xz(yz)
Kxy → x 
Ix → x

그러므로, 예를들어 SKKI 가 있다면, 다음의 과정을 거쳐서 K 가 됩니다.

SKKI → KK(KI) → K

자세한 내용은 http://en.wikipedia.org/wiki/SKI_combinator_calculus 를 참조하시기 바랍니다.

(2) 명세(specification)

이제부터 ghci 에서 동작하는 SKI 연산 시뮬레이터를 만들 것입니다.

다음과 같은 방식으로 동작합니다.

*SKI> S :@ K :@ S :@ K
SKSK
*SKI> eval 7 $ S :@ K :@ S :@ K
K
*SKI> trace $ S :@ K :@ S :@ K
SKSK
--> KK(SK)
--> K

eval n 은 최대 n단계에 걸쳐 계산하는 함수입니다. SKI 연산은 자칫 무한루프에 빠질 수 있기 때문에, 이런 함수가 필요합니다.

trace 함수는 계산과정을 편리하게 보여주는 함수입니다.

(3) GADT 와 Show

이제 GADT 로 새로운 자료형을 정의해봅시다.

S, K, I 가 있어야겠고, 이들을 연결시켜주는 (:@) 생성자도 필요합니다.

module SKI where
data SKI where
    S :: SKI
    K :: SKI
    I :: SKI
    (:@) :: SKI -> SKI -> SKI
infixl 6 :@

이 모듈은 오류는 발생하지 않지만, 이것만으로는 SKI 자료형을 출력하는 것이 불가능합니다.

그러므로 show 함수를 정의해서, SKI 자료형을 어떻게 출력해야하는지를 ghci 에게 알려줘야합니다.

instance Show SKI where
    show (S) = "S"
    show (K) = "K"
    show (I) = "I"

이렇게 하면 S, K, I 는 출력할 수 있습니다.

*SKI> S
S
*SKI> K
K
*SKI> I
I

그리고 다음 코드를 추가하면

    show (a :@ b) = show a ++ show b

다음과 같이 :@ 로 결합된 경우도 출력할 수 있습니다.

*SKI> S :@ K
SK
*SKI> S :@ K :@ I
SKI

하지만 다음과 같이 괄호가 있는 경우에는 정확히 출력되지 않습니다. S(KI) 로 출력돼야합니다.

*SKI> S :@ (K :@ I)
SKI

다음 코드를 show (a :@ b) = show a ++ show b 의 바로 위에 두어서 엉뚱하게 출력되는 경우를 막아야 합니다.

    show (t1 :@ (t2 :@ t3)) = show t1 ++ "(" ++ show (t2 :@ t3) ++ ")"

이제는 제대로 출력됩니다.

*SKI> S :@ (K :@ I)
S(KI)

(4) 연산규칙 정의 - eval 함수

eval 함수는 SKI 연산을 실제로 수행하는 함수입니다.

eval :: Int -> SKI -> SKI
eval 0 x = x   -- 첫번째 인자가 0 이면 연산을 중단합니다.
eval n (S :@ x :@ y :@ z) = eval (n-1) (x :@ z :@ (y :@ z))   -- S 연산규칙
eval n (K :@ x :@ y) = eval (n-1) x   -- K 연산규칙
eval n (I :@ x) = eval (n-1) x   -- I 연산규칙
eval n (x :@ y) = eval (n-1) $ (eval n x) :@ (eval n y)   -- 위의 연산규칙을 재귀적으로 적용시켜 줍니다. 
eval _ x = x   -- 위의 어떤 경우에도 해당되지 않는다면 연산을 중단합니다.

불과 7줄로 eval 함수의 정의가 완벽하게 끝났습니다.

*SKI> eval 7 $ S :@ K :@ S :@ K
K

SKKI → KK(KI) → K 이므로 잘 동작하는 것으로 보입니다.

몇 가지 경우를 더 입력해서 테스트하는 것은 각자 해보시기 바랍니다.

(5) 마무리 - trace 함수

trace 함수는 단순해서 별다른 설명이 필요없어 보입니다.

_trace :: Int -> SKI -> String
_trace 0 x = show x
_trace n x =
    if (show $ eval n x) == (show $ eval (n-1) x)
    then (_trace (n-1) x)
    else (_trace (n-1) x) ++ "\n--> "  ++ (show $ eval n x)
 
trace = putStrLn . (_trace 7)

(6) 실행결과

자, 이제 다됐으니 SKI 연산과정을 감상해봅시다.

*SKI> trace $ S :@ K :@ S :@ K
SKSK
--> KK(SK)
--> K
 
*SKI> trace $ S :@ I :@ I :@ (K :@ K)
SII(KK)
--> I(KK)(I(KK))
--> KK(KK)
--> K
 
*SKI> trace $ S :@ I :@ I :@ (S :@ I :@ I)
SII(SII)
--> I(SII)(I(SII))
--> SII(SII)
--> I(SII)(I(SII))
--> SII(SII)
--> I(SII)(I(SII))
--> SII(SII)
--> I(SII)(I(SII))
 
*SKI> trace $ S :@ I :@ I :@ (S :@ (K :@ K) :@ (S :@ I :@ I))
SII(S(KK)(SII))
--> I(S(KK)(SII))(I(S(KK)(SII)))
--> S(KK)(SII)(S(KK)(SII))
--> KK(S(KK)(SII))(SII(S(KK)(SII)))
--> K(I(S(KK)(SII))(I(S(KK)(SII))))
--> K(KK(S(KK)(SII))(SII(S(KK)(SII))))
--> K(K(K(I(S(KK)(SII))(I(S(KK)(SII))))))
--> K(K(K(K(K(K(S(KK)(SII)(S(KK)(SII))))))))

그리고 직접 코드를 작성해보면서 내용을 따라가는 것이 가장 좋겠지만,

단지 잘 동작하는지만을 확인하고 싶은 분들을 위해서 소스코드 ski.hs 를 압축하여 첨부합니다.



5. 예제 2 : 리스트? 튜플?

(다음에 계속 ...)

File attachments: 
첨부파일 크기
Binary Data ski.hs_.tar.gz610바이트
Forums: 
imyejin의 이미지

이거 대학교 학교 수업이나 대학원 연구랑 관련된 내용인가요, 아니면 그냥 재미로 혼자 공부하시는 건가요?
학교 수업이나 연구 관련이라면 어느 학교인지, 뭐 구체적으로 말씀하시기 곤란하시면 우리나라 학교인지 아니면 다른 어느 나라에 있는지라도 궁금하군요 ~

용어에 대해서 한 가지 좀 헷갈릴 소지가 있는 것이 있는데, 추상적 자료형(abstract data type)이라는 말은 함수형 언어에서는 보통 모듈 타입(module type)과 동의어이며 모듈 타입은 existential type 으로 나타내는 경우가 많기 때문에 abstract data type 과 module type 그리고 existential type 이렇게 세 용어가 서로 비슷하게 쓰입니다. 글에서 언급한 타입 변수를 포함하는 데이타 타입은 여러모양 타입(polymorphic type) 혹은 다른 타입을 인자로 받는 타입(parametrized type) 등으로 표현하는 것이 일반적입니다. 링크하신 http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType 글 에서도 abstract type 은 분명 polymorphic type 혹은 parametrized type 과는 다른 뜻으로 쓰이고 있음을 확인할 수 있습니다.

또한 GADT를 쓰면 일반적으로 타입 유추(type inference)가 불가능하기 때문에 함수를 정의할 때 타입 선언이 필수적이라는 점도 문서에 언급했으면 합니다.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

feanor의 이미지

좋은 글 감사합니다.

SKI를 출력하는 부분에서 "instance Show (Term x) where"로 되어 있는데 글을 쓰시다가 갱신이 안 된 듯 합니다. 첨부하신 파일에는 "instance Show SKI where"로 제대로 되어 있습니다.

redneval의 이미지

1. abstract data type

먼저 말씀드릴 것은,

저는 혼란을 피하기 위해서, 하스켈 위키(http://www.haskell.org/haskellwiki)에 나온 설명을 (비판없이) 그대로 따른다는 점입니다.

(물론 하스켈 위키가 정확하지 않다라고 하시면, 할말이 없어지겠습니다만.)

그러므로 다른 함수형 언어에서의 설명과 차이가 있을 수 있습니다.

이점은 이해를 해주시기를 바라며,

하스켈 위키에서는 다음과 같이 설명이 돼있습니다.

abstract data type == parameterized data type (http://www.haskell.org/haskellwiki/Abstract_data_type)

abstract data type != extential type (http://www.haskell.org/haskellwiki/Existential_types)

그리고 적어도 하스켈에서는 data type 과 type 을 다르게 보고있습니다.

http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeType

에서도 설명이 나와있듯이, data type 은 type 의 한 종류입니다.

abstract data type 과 abstract type 는 별개로 생각해야하지 않을까 싶습니다. (<-- 이 부분은 순전히 제 생각임.)

2. 형 선언 (type declaration)

좋은 지적이십니다.

다만, GADT 도 완벽히 형 유추 (type inference) 가 가능하다는 주장이 있습니다.

(http://tomschrijvers.blogspot.com/2009/03/complete-and-decidable-type-inferennce.html)

그리고 본 글에서 다루는 예제의 경우는 타입 선언이 필수적이지는 않습니다. :)

어쨌든, `GHC 에서는 GADT 를 사용하면 형 유추가 완벽하지 않으므로, 함수를 정의할 때 형 선언을 해주는 것이 좋다.'

정도로 (다음번에) 적어주면 되겠네요.

사실은 `모든 함수에 형 선언을 해주는 것'이 좋은 코딩 습관이고,

이쪽을 더 강조하고 싶기 때문에 어차피 저에게는 별로 큰 의미는 없습니다만.

3. Just for fun. 그냥 재미로 혼자 공부하고 있습니다.

4. 오타는 수정했습니다.

"instance Show (Term x) where" -> "instance Show SKI where"

--------------------Signature--------------------
Light a candle before cursing the darkness.

imyejin의 이미지

1번에 대해서는 abstract data type 과 abstract type 을 다르게 해석하는 것이 맞겠군요.

2번에 언급한 논문은 abstract를 읽어봐도 아시겠지만 "모든" GADT를 사용하는 프로그램 대해서 형 유추 (type inference)를 다 할 수 있다는 주장이 결코 아니라, "일부" GADT를 사용하는 프로그램에 대해서 complete 하고 decidable 한 타입 유추 알고리듬을 소개하는 논문이며, 예전보다 좀더 간단한 알고리듬이라는 장점이 있는 정도입니다. 곧 GHC 알고리듬을 저걸로 바꿔서 구현하겠죠. (제목만 보면 오해할 소지가 크다는 점에서 약간 낚시성이라능 ~~~)

그리고 본문에 언급한 예제에 대해서는 타입 선언이 필수적이지 않은 것은 사실상 GADT의 추가 기능을 전혀 이용하고 있지 않기 때문이죠. ADT로 선언해도 될 SKI 타입을 문법만 GADT를 사용한 것 뿐이잖습니까? -_-;; 다음 번에는 GADT의 기능을 제대로 이용하는 예제를 추가해 주세요! 하스켈 위키에 나온 SK combinator calculus를 GADT로 정의하는 Term a 타입은 제대로 GADT 기능을 이용한 예제인데 그것을 그대로 가져다가 소개하는 것도 좋고요.

참고로 GHC 구현이 일부 GADT에 대해서는 타입을 유추해 줄 수 타입 유추 알고리듬을 사용하고 있기 때문인데, 저런 논문도 나오고 타입유추 알고리듬이 계속 바뀌는 중이라 호환성을 위해서는 GADT를 사용하면 타입 선언을 해 주는 게 나중을 위해서도 좋습니다. 타입유추 알고리듬 업데이트 하고 난 다음 번 버전에서 타입 유추가 된다는 보장이 없으니까요. 본문과 같이 비교적 간단한 예제의 경우는 뭐 안될 일이 솔직히 없다고 생각하긴 하지만, 말씀하신 대로 특히 GADT를 사용하는 경우에는 타입 정보가 더 복잡해지고 또 프로그램이 만족해야 할 조건을 더 상세히 기술하기 때문에 문서화의 측면해서도 선언을 해 주는 게 좋겠죠.

@ 한가지 또 용어 문제를 덧붙이자면 GADT를 소개하면서 나온 주석을 다음과 같이 고쳤으면 좋겠습니다.

-- ADT 방식 (실행시 오류 발생)

아마도 ghci를 실행해서 저런 데이타 타입 정의가 있는 파일을 불러와 컴파일하다가는 오류가 발생한다는 뜻으로 쓰신 것 같은데, 그냥 저렇게만 써 놓으면 컴파일은 다 되는데 eval 함수를 실행하다 런타임 오류가 난단 말인가 이렇게도 오해할 수 있기 때문에

-- ADT 방식 (컴파일 오류 발생)

이라고 하는 것이 더 좋지 않을까 생각합니다.

@@ 참고로 unlambda라는 반쯤은 장난인 엽기적인 언어가 바로 이 SKI combinator calculus를 바탕으로 하고 있습니다 http://www.madore.org/~david/programs/unlambda/ 언람다는 무려 데비안 패키지까지 제공되기 때문에 apt-get install unlambda 로 설치할 수 있죠 -_-;;

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

차리서의 이미지

imyejin wrote:
그리고 본문에 언급한 예제에 대해서는 타입 선언이 필수적이지 않은 것은 사실상 GADT의 추가 기능을 전혀 이용하고 있지 않기 때문이죠. ADT로 선언해도 될 SKI 타입을 문법만 GADT를 사용한 것 뿐이잖습니까? -_-;; 다음 번에는 GADT의 기능을 제대로 이용하는 예제를 추가해 주세요! 하스켈 위키에 나온 SK combinator calculus를 GADT로 정의하는 Term a 타입은 제대로 GADT 기능을 이용한 예제인데 그것을 그대로 가져다가 소개하는 것도 좋고요.

요즘은 KLDP에 자주 못 오지만, 올 때마다 imyejin님의 글들은 꼭 챙겨서 보고있습니다. redneval님의 글도 계속 감사히 구독하겠습니다. :^)

각설하고, 마침 좋은 기회가 될 것 같아서 저도 한 번 정중히 부탁드려봅니다. 기왕 GADT에 관해 좋은 글을 올려주시는 김에 (그리고 imyejin님도 기왕 좋은 조언을 달아주시는 김에), 현재 Haskell 진영의 GADT를 통한 투쟁이 어디까지 와있는지 (bleeding edge까지는 아니더라도) 좀 더 구체적으로 구경해볼 수 있으면 좋겠습니다. 살짝 부연해보자면,

  • 명세력 측면에서 거의 이상적인 λPω 기반의 proof assistant들(LEGO, Coq)은 증명의 부담이 문제고,
  • 적당한 명세력에 형검사의 자동화도 나름 신경썼다는 (λP 이상 기반의) 자칭 범용 PL들(Agda2, Epigram 등)은 annotation이 문제거나 본질적으로 proof assistant가 간판만 바꿔붙였을 뿐이니,
이와 비교해서 System F 기반의 '진짜' 범용 PL들은 GADT 등의 우회법을 통해 어떤 성취를 이루고있는지 그 동향이 궁금합니다.

개인적으로 최근에 다른 부분에 집중하고있어서 Haskell 진영의 행보를 추적하지 못한지 좀 됐고 아마 앞으로도 당분간은 제대로 쫓아가지 못할 상황이어서, 이 글타래를 발견하는 순간 욕심이 생겼습니다만, 어디까지나 제 일방적인 '부탁'일 뿐입니다. 어떤 방향으로 집필/조언해주셔도 그저 감사히 읽고 공부하겠습니다. ^^;

PS: 혹시 수정 전의 장문(長文)을 보신 분이 계시다면 죄송합니다. 졸려서 그냥 자려다가 아무래도 너무 심했다 싶어서 요점만 남기고 싹 정리했습니다. ^^;;

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

imyejin의 이미지

최근 캐나다 몬트리올 대학의 박사과정 학생의 type preserving compiler 관련 연구를 보시면 GADT를 비롯한 GHC의 타입 시스템 확장의 활용에 대한 모든 것은 아니더라도 많은 것을 보실 수 있습니다. http://www-etud.iro.umontreal.ca/~guillelj/ 이런 문제를 되도록 손쉽고 타입 안전성이 자동으로 증명되는 코드를 만들기 위해서 여러가지 타입 시스템 확장을 연구하고 있다고 보시면 됩니다.

그리고 아마도 아시겠지만 유럽에서 Ralf Hinze 같은 사람들이 data type generic programming 을 GADT를 이용해서 코딩하는 예제 같은 걸 많이 만들어서 보여주고 있고요, 이번 겨울에 한국서 열리는 APLAS 2009 http://ropas.snu.ac.kr/aplas09/ 에서 이 Ralf Hinze 라는 분이 프로그램 커미티인 걸로 나와 있으니 아마도 학회에 나타나시겠죠. 사실 이 분과 직접 대화를 해 보시면 아마 그런 쪽으로 더 많은 이야기를 들을 수 있을 것입니다.

그러니까 아직 System F 혹은 System Fw 기반 혹은 lambda cube나 PTS의 다른 어떤 지점에 있는 좋은 디자인의 범용 프로그래밍 언어를 위한 연구는 계속 진행중에 있고, 하스켈 진영에서는 에서는 일단 First Class Polymorphism 및 Rank-N polymorphism 그리고 GADT 같은 타입 시스템 확장을 GHC에 추가해서 시험해 보고 하스켈의 다음 표준 Haskell' (하스켈 프라임)에 어떤 식으로 반영할 것인가가 주요 이슈입니다.

@ 자동 증명기와 함수형 언어 가운데쯤에 있는 실용적인 언어가 대중화되면 여러가지 문제(어디까지 타입 유추를 할 수 있고 언제 사용자가 타입을 명세해야 하는가, 컴파일할 때 실행 시간에 필요없는 타입 정보를 어떻게 찾아서 제거할 것인가, 부수적으로 필요한 증명으로 쓰일 타입들 간의 관계를 명시하는 코드에 대한 termination 및 totalness 등 추가적인 조건 검사)에 대한 해법이 다 나와서 한꺼번에 해결이 된 다음, 또 그런 것들을 잘 조합하는 디자인이 있어야 하는 문제니까요.

임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

[예진아씨 피카사 웹앨범] 임예진 팬클럽 ♡예진아씨♡ http://cafe.daum.net/imyejin

차리서의 이미지

imyejin wrote:
하스켈 진영에서는 에서는 일단 First Class Polymorphism 및 Rank-N polymorphism 그리고 GADT 같은 타입 시스템 확장을 GHC에 추가해서 시험해 보고 하스켈의 다음 표준 Haskell' (하스켈 프라임)에 어떤 식으로 반영할 것인가가 주요 이슈입니다.

대충 1년 이상 지난 오래된 정보이긴 합니다만, Haskell'은 이미 (수정이 아닌 '신규 추가'는 더이상 반영되기 힘든) 일종의 동결 모드에 들어간 것으로 알고있고 그간 구현물 진영에서 이미 성과를 낸 제안들 중 다수가 받아들여지지 않을 분위기였습니다. 특히 HM 타입시스템의 '봉인'에 대한 저항이나 System F 자체의 한계점을 돌파하려는 노력들은 대부분 rejected 혹은 undecided였고, GADT의 경우 확실친 않습니다만 기억이 맞다면 아마 undecided였을겁니다.

개인적으로는 위원회의 완고한 학술적 행보를 선호하는 편이지만, 위원회 어르신들의 면면을 유심히 살펴보면 그 완고함의 이유를 조금 색다르게 갖다붙여볼 수도 있을 것 같습니다. John McCarthy의 작고 아름다운 core만으로 Common LISP이라는 거대 굇수를 소환해내는 '참극'을 직접 목격했거나 저지른 세대니, Haskell에서 만큼은 같은 만행을 반복하지 않으려는건지도 모르죠. :^P

물론, 마지막 문장은 반쯤은 농담입니다. 부디 정색하고 불쾌해하는 분 없으시길... ^^;

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

--
자본주의, 자유민주주의 사회에서는 결국 자유마저 돈으로 사야하나보다.
사줄테니 제발 팔기나 해다오. 아직 내가 "사겠다"고 말하는 동안에 말이다!

죠커의 이미지

오프토픽이지만 Common Lisp이 거대 괴수는 아네요 =3=3=

- 죠커's blog / HanIRC:#CN

댓글 달기

Filtered HTML

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

BBCode

  • 텍스트에 BBCode 태그를 사용할 수 있습니다. URL은 자동으로 링크 됩니다.
  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param>
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.

Textile

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • You can use Textile markup to format text.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Markdown

  • 다음 태그를 이용하여 소스 코드 구문 강조를 할 수 있습니다: <code>, <blockcode>, <apache>, <applescript>, <autoconf>, <awk>, <bash>, <c>, <cpp>, <css>, <diff>, <drupal5>, <drupal6>, <gdb>, <html>, <html5>, <java>, <javascript>, <ldif>, <lua>, <make>, <mysql>, <perl>, <perl6>, <php>, <pgsql>, <proftpd>, <python>, <reg>, <spec>, <ruby>. 지원하는 태그 형식: <foo>, [foo].
  • Quick Tips:
    • Two or more spaces at a line's end = Line break
    • Double returns = Paragraph
    • *Single asterisks* or _single underscores_ = Emphasis
    • **Double** or __double__ = Strong
    • This is [a link](http://the.link.example.com "The optional title text")
    For complete details on the Markdown syntax, see the Markdown documentation and Markdown Extra documentation for tables, footnotes, and more.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 사용할 수 있는 HTML 태그: <p><div><span><br><a><em><strong><del><ins><b><i><u><s><pre><code><cite><blockquote><ul><ol><li><dl><dt><dd><table><tr><td><th><thead><tbody><h1><h2><h3><h4><h5><h6><img><embed><object><param><hr>

Plain text

  • HTML 태그를 사용할 수 없습니다.
  • web 주소와/이메일 주소를 클릭할 수 있는 링크로 자동으로 바꿉니다.
  • 줄과 단락은 자동으로 분리됩니다.
댓글 첨부 파일
이 댓글에 이미지나 파일을 업로드 합니다.
파일 크기는 8 MB보다 작아야 합니다.
허용할 파일 형식: txt pdf doc xls gif jpg jpeg mp3 png rar zip.
CAPTCHA
이것은 자동으로 스팸을 올리는 것을 막기 위해서 제공됩니다.