다음 forall
과 같이 소위 “존재 유형”에서 키워드가 사용되는 방식을 이해하기 시작 했습니다.
data ShowBox = forall s. Show s => SB s
그러나 이것은 forall
사용 방법의 일부일 뿐이며 다음과 같은 용도로 내 마음을 감쌀 수는 없습니다.
runST :: forall a. (forall s. ST s a) -> a
또는 왜 이것이 다른지 설명하십시오.
foo :: (forall a. a -> a) -> (Char, Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
아니면 모든 RankNTypes
것들 …
학업 환경에서 일반적으로 사용되는 언어보다는 명확하고 전문 용어가없는 영어를 선호합니다. 내가 이것에 대해 읽으려고 시도하는 대부분의 설명 (검색 엔진을 통해 찾을 수있는 설명)에는 다음과 같은 문제가 있습니다.
- 그들은 불완전하다. 이 키워드 (예 : “기존 유형”) 사용의 한 부분을 설명합니다.이 키워드는 완전히 다른 방식 (예
runST
:foo
등bar
) 으로 사용하는 코드를 읽을 때까지 기분이 좋아 집니다. - 그들은 이번 주에 인기가 많은 이산 수학, 범주 이론 또는 추상 대수학에서 최신을 읽었다는 가정으로 가득 차 있습니다. (내가 “종이에 무엇이든 상담하십시오”라는 단어를 읽지 않으면 구현 내용에 대해 너무 빠릅니다.)
- 그것들은 간단한 개념조차도 자주 왜곡되고 문법과 의미론으로 변형시키는 방식으로 작성되었습니다.
그래서…
실제 질문에. forall
내가 전문 용어에 가파른 수학 자라고 가정하지 않는 사람 이 명확하고 평범한 영어로 키워드를 완전히 설명 할 수 있습니까 ?
추가하기 위해 편집 :
아래의 고품질 답변에서 두 가지 뛰어난 답변이 있었지만 불행히도 하나만 가장 잘 선택할 수 있습니다. Norman의 답변 은 상세하고 유용하며 이론적 인 토대를 forall
보여 주면서 동시에 그에 대한 실제적인 의미를 보여줍니다. yairchu의 답변다른 언급되지 않은 영역 (범위 유형 변수)을 다루고 코드와 GHCi 세션으로 모든 개념을 설명했습니다. 최선을 다해서 선택할 수 있었으면 좋겠다. 불행히도 나는 두 대답을 자세히 살펴본 후에는 설명 코드와 설명으로 인해 yairchu가 Norman의 것보다 약간 우위에 있다고 결정했습니다. 그러나 이것은 forall
유형 불일치로 볼 때 희미한 느낌 이 들지 않는 지점까지 이것을 이해하기 위해 두 가지 대답이 필요했기 때문에 약간 불공평 합니다.
답변
코드 예제로 시작해 봅시다.
foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
foob postProcess onNothin onJust mval =
postProcess val
where
val :: b
val = maybe onNothin onJust mval
이 코드는 일반 Haskell 98에서 컴파일 (구문 오류)되지 않습니다 forall
. 키워드 를 지원하려면 확장이 필요합니다 .
기본적으로,이 셋 개이다 다른 일반적인에 사용하는 forall
키워드 (또는 적어도 그렇게 보인다는 ), 각 자체 하스켈 확장이 있습니다 ScopedTypeVariables
, RankNTypes
/ Rank2Types
, ExistentialQuantification
.
위의 코드는 활성화 된 구문 검사 중 오류가 발생하지 않고 활성화 된 유형 검사 만 수행합니다 ScopedTypeVariables
.
범위가 지정된 유형 변수 :
범위가 지정된 유형 변수는 코드 내부 where
절의 유형을 지정하는 데 도움이됩니다 . 그것은을 만들어 b
에 val :: b
는 AS 동일한 것을 b
에서 foob :: forall a b. (b -> b) -> b -> (a -> b) -> Maybe a -> b
.
혼란스러운 점 : forall
유형에서 생략 할 때 실제로 여전히 암시 적이라고 들릴 수 있습니다 . ( 노먼의 대답에서 : “일반적으로 이러한 언어는 다형성 유형에서 전체를 생략합니다” ). 이 주장은 정확 하지만 사용이 forall
아닌 다른 용도를 나타냅니다 ScopedTypeVariables
.
순위 -N- 타입 :
그것부터 시작하자 mayb :: b -> (a -> b) -> Maybe a -> b
에 해당합니다 mayb :: forall a b. b -> (a -> b) -> Maybe a -> b
, 를 제외시켰다 때를 위해 ScopedTypeVariables
사용할 수 있습니다.
이것은 모든 작동한다는 것을 의미 a
하고 b
.
이런 식으로하고 싶다고 가정 해 봅시다.
ghci> let putInList x = [x]
ghci> liftTup putInList (5, "Blah")
([5], ["Blah"])
이것의 유형은 무엇입니까 liftTup
? 이것의liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
. 이유를 알아 보려면 코드를 작성해 보겠습니다.
ghci> let liftTup liftFunc (a, b) = (liftFunc a, liftFunc b)
ghci> liftTup (\x -> [x]) (5, "Hello")
No instance for (Num [Char])
...
ghci> -- huh?
ghci> :t liftTup
liftTup :: (t -> t1) -> (t, t) -> (t1, t1)
“흠. 왜 GHC는 튜플에 같은 유형의 두 개가 포함되어야한다고 추론 하는가?
-- test.hs
liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)
ghci> :l test.hs
Couldnt match expected type 'x' against inferred type 'b'
...
흠. 그래서 여기 GHC은 우리가 적용 할 수 없습니다 liftFunc
에 v
있기 때문에 v :: b
와 liftFunc
을 원한다 x
. 우리는 함수가 가능한 모든 함수를 받아들이기를 원합니다.x
!
{-# LANGUAGE RankNTypes #-}
liftTup :: (forall x. x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)
그래서 그렇지 않습니다 liftTup
모든 것이 작동 x
하지는 않습니다. 그것이 얻는 기능입니다.
기존 정량화 :
예를 들어 봅시다 :
-- test.hs
{-# LANGUAGE ExistentialQuantification #-}
data EQList = forall a. EQList [a]
eqListLen :: EQList -> Int
eqListLen (EQList x) = length x
ghci> :l test.hs
ghci> eqListLen $ EQList ["Hello", "World"]
2
Rank-N-Types와 다른 점은 무엇입니까?
ghci> :set -XRankNTypes
ghci> length (["Hello", "World"] :: forall a. [a])
Couldnt match expected type 'a' against inferred type '[Char]'
...
Rank-N-Types를 사용하면 forall a
식이 가능한 모든에 맞아야합니다 a
. 예를 들면 다음과 같습니다.
ghci> length ([] :: forall a. [a])
0
빈 목록은 모든 유형의 목록으로 작동합니다.
그래서 실존-정량화와 함께, forall
에이야 data
정의는 그 의미, 값이 포함되어 있습니다 될 어떤 그렇지 않은 것을, 적절한 형태 해야 될 모든 적절한 유형.
답변
누구나 forall 키워드를 명확하고 평범한 영어로 완전히 설명 할 수 있습니까 ?
아닙니다. (돈 스튜어트가 할 수도 있습니다.)
다음은 간단하고 명확한 설명의 장벽입니다 forall
.
-
수량 자입니다. 당신은 보편적이거나 존재하는 정량자를 보도록 최소한 작은 논리 (술어 미적분학)를 가져야합니다. 술어 미적분학을 본 적이 없거나 정량 자에 익숙하지 않은 경우 (그리고 박사 학위 자격 시험 중에 불편한 학생들을 보았습니다), 당신에게는 쉬운 설명이 없습니다
forall
. -
그것은 A의 형 정량. System F를 보지 못하고 다형성 유형을 작성하는 연습을 받았다면
forall
혼란 스러울 것입니다. Haskell 또는 ML에 대한 경험으로는 충분하지 않습니다. 일반적으로 이러한 언어forall
는 다형성 유형에서 생략되기 때문 입니다. (제 생각에 이것은 언어 설계 실수입니다.) -
특히 Haskell에서는
forall
혼란스러워하는 방식으로 사용됩니다. (저는 유형 이론가는 아니지만 제 작품은 많은 유형 이론 과 접촉 하게되며 매우 편합니다.) 저에게 혼란의 주요 원인은 다음과forall
같은 유형을 인코딩하는 데 사용됩니다. 나는 나 자신과 함께 쓰는 것을 선호한다exists
. 그것은 정량 자와 화살표를 포함하는 까다로운 유형의 동 형사상으로 정당화되며, 그것을 이해하고 싶을 때마다, 나는 사물을 직접 찾아서 동 형사상을 해결해야합니다.유형 동 형사상 개념에 익숙하지 않거나 유형 동 형사상에 대해 생각하는 연습이 없다면,이 사용은
forall
당신을 좌절시킬 것입니다. -
의 일반적인 개념
forall
은 항상 동일하지만 (유형 변수를 도입하기위한 바인딩) 다른 용도의 세부 사항은 크게 다를 수 있습니다. 비공식 영어는 변형을 설명하는 데 유용한 도구가 아닙니다. 무슨 일이 일어나고 있는지 이해하려면 수학이 필요합니다. 이 경우 관련 수학은 Benjamin Pierce의 입문 텍스트 유형 및 프로그래밍 언어 에서 찾을 수 있습니다 .
귀하의 특정 예에 관해서는
-
runST
머리를 아프게 해야 합니다. 더 높은 순위의 유형 (화살표 왼쪽 끝)은 야생에서 거의 발견되지 않습니다. 나는 소개 된 종이 읽어 보시기 바랍니다runST
: “게으른 기능 상태 스레드” . 이것은 정말 좋은 논문이며,runST
특히 유형과 일반적으로 상위 유형에 대해 훨씬 더 나은 직관을 제공합니다 . 설명은 여러 페이지를 차지하며 잘 완료되었으며 여기에 요약하려고하지 않습니다. -
치다
foo :: (forall a. a -> a) -> (Char,Bool) bar :: forall a. ((a -> a) -> (Char, Bool))
호출
bar
하면 원하는 유형a
을 간단히 선택할 수 있으며 유형 에서 유형a
으로 함수를 전달할 수 있습니다a
. 예를 들어, 함수(+1)
또는 함수를 전달할 수 있습니다reverse
. 당신은forall
“지금 유형을 고를 수 있습니다”라고 생각할 수 있습니다 . 유형 선택에 대한 기술 단어는 인스턴스화 입니다.호출에 대한 제한
foo
은 훨씬 더 엄격합니다. 인수 는 다형성 함수foo
여야합니다 . 이 유형의 유일한 기능은 내가하는 통과 할 수foo
있습니다id
또는 기능이 항상 발산 또는 오류 같은undefined
. 그 이유는과이다foo
, (가)forall
의 호출도록 화살표의 왼쪽에foo
내가 어떤 선택을하지 않는a
것이다 – 오히려 그것은의 구현 의foo
그 무엇을 선택하는 얻을 수a
있다는. 에서forall
와 같이 화살표 위가 아니라 화살표 왼쪽에 있기 때문에bar
인스턴스화는 호출 사이트가 아닌 함수 본문에서 발생합니다.
요약 : 전체 의 설명 forall
키워드는 수학을 필요로하며, 단지 수학을 공부 한 사람에 의해 이해 될 수있다. 부분적인 설명조차도 수학 없이는 이해하기 어렵습니다. 그러나 어쩌면 부분적인 비 수학 설명이 약간 도움이 될 수 있습니다. Launchbury와 Peyton Jones를 읽어보십시오 runST
!
부록 : 전문 용어 “위”, “아래”, “왼쪽”. 이것들은 타입이 작성 되는 텍스트 방식과 추상 구문 트리와 관련이 없습니다. 추상 구문에서 a forall
는 유형 변수의 이름을 취한 다음 전체 유형 아래에 전체 유형이 있습니다. 화살표는 두 가지 유형 (인수 및 결과 유형)을 사용하여 새로운 유형 (함수 유형)을 형성합니다. 인수 유형은 화살표의 “왼쪽”입니다. 추상 구문 트리에서 화살표의 왼쪽 자식입니다.
예 :
-
에서
forall a . [a] -> [a]
, forall은 화살표 위에 있습니다. 화살표 왼쪽에있는 것은[a]
입니다. -
에
forall n f e x . (forall e x . n e x -> f -> Fact x f) -> Block n e x -> f -> Fact x f
괄호 안의 유형은 “화살표의 왼쪽으로 forall”이라고합니다. (저는 작업중 인 최적화 프로그램에서 이와 같은 유형을 사용하고 있습니다.)
답변
내 원래 답변 :
누구나 forall 키워드를 명확하고 평범한 영어로 완전히 설명 할 수 있습니까?
Norman이 지적했듯이, 유형 이론에서 기술 용어에 대한 명확하고 명확한 영어 설명을 제공하는 것은 매우 어렵습니다. 우리 모두 노력하고 있습니다.
‘forall’에 대해 기억해야 할 것은 한 가지뿐입니다 . 유형을 일부 범위에 바인딩합니다 . 일단 이해하면 모든 것이 매우 쉽습니다. 형식 수준에서 ‘람다'(또는 ‘let’의 형태)와 동일합니다. Norman Ramsey는 “왼쪽”/ “위”라는 개념을 사용하여 이와 동일한 범위의 개념을 뛰어난 답변 으로 전달합니다 .
‘forall’의 대부분의 사용은 매우 간단 하며 GHC 사용자 매뉴얼 S7.8에 소개되어 있으며 특히 중첩 된 ‘forall’형식의 우수한 S7.8.5 에 소개되어 있습니다.
Haskell에서는 일반적으로 유형이 보편적으로 질화 될 때 유형에 대한 바인더를 제거합니다.
length :: forall a. [a] -> Int
다음과 같습니다.
length :: [a] -> Int
그게 다야.
이제 유형 변수를 일부 범위에 바인딩 할 수 있기 때문에 데이터 구조 내에서만 유형 변수가 표시되는 첫 번째 예와 같이 최상위 수준 이외의 범위 ( ” 일반적으로 정량화 된 “)를 가질 수 있습니다 . 이것은 숨겨진 유형 ( ” 존재 유형 “)을 허용합니다. 또는 임의 의 바인딩 중첩 ( “랭크 N 유형”)을 가질 수 있습니다 .
타입 시스템을 깊이 이해하려면 전문 용어를 배워야합니다. 이것이 컴퓨터 과학의 본질입니다. 그러나 위와 같이 단순한 사용은 가치 수준에서 ‘let’을 사용하여 직관적으로 파악할 수 있어야합니다. 훌륭한 소개는 Launchbury와 Peyton Jones 입니다.
답변
그들은 이번 주에 인기있는 이산 수학, 범주 이론 또는 추상 대수학의 모든 지점에서 최신을 읽었다는 가정으로 가득 차 있습니다. ( ‘구현 내용에 대해 무엇이든 논문을 참고하십시오’라는 단어를 다시 읽지 않으면 너무 빠릅니다.)
어, 그리고 간단한 1 차 로직은 어떻습니까? forall
는 보편적 인 정량화 와 관련하여 매우 명확하며 , 문맥에서 실존 적이라는 용어도 더 의미가 있지만 exists
키워드 가 있으면 다소 어색합니다 . 정량화가 효과적으로 보편적인지 실존 적인지 여부는 기능 화살표의 어느 쪽에서 변수가 사용되는지에 대한 정량화 기의 배치에 따라 달라지며 모두 약간 혼란 스럽습니다.
따라서 이것이 도움이되지 않거나 상징적 논리를 좋아하지 않는다면 더 기능적인 프로그래밍 관점에서 유형 변수를 함수에 대한 (암시 적) 유형 매개 변수로 생각할 수 있습니다 . 이런 의미에서 형식 매개 변수를 사용하는 함수는 전통적으로 어떤 이유로 든 대문자 람다를 사용하여 작성됩니다 /\
.
따라서 id
기능을 고려하십시오 .
id :: forall a. a -> a
id x = x
“type 매개 변수”를 유형 시그니처에서 옮기고 인라인 유형 주석을 추가하여 람다로 다시 작성할 수 있습니다.
id = /\a -> (\x -> x) :: a -> a
다음과 같은 작업을 수행합니다 const
.
const = /\a b -> (\x y -> x) :: a -> b -> a
따라서 bar
함수는 다음과 같습니다.
bar = /\a -> (\f -> ('t', True)) :: (a -> a) -> (Char, Bool)
bar
인수로 제공된 함수의 유형은 bar
의 유형 매개 변수 에 따라 다릅니다 . 대신 이와 같은 것이 있는지 고려하십시오.
bar2 = /\a -> (\f -> (f 't', True)) :: (a -> a) -> (Char, Bool)
다음 bar2
은 함수를 type에 적용하는 Char
것이므로 bar2
type 매개 변수 이외의 다른 형식 매개 변수 Char
를 지정하면 형식 오류가 발생합니다.
반면에 foo
다음과 같이 보일 수 있습니다.
foo = (\f -> (f Char 't', f Bool True))
달리 bar
, foo
실제로 모든에서 모든 유형의 매개 변수를 고려하지 않습니다! 자체적 으로 유형 매개 변수를 사용 하는 함수를 취한 다음 해당 함수를 서로 다른 두 가지 유형에 적용합니다 .
따라서 forall
타입 시그니처에서 를 볼 때 , 타입 시그너처에 대한 람다 식 으로 생각하십시오 . 일반 람다와 마찬가지로 범위는 forall
가능한 한 오른쪽으로 확장되고 괄호로 확장되며 , 일반 람다에 바인딩 된 변수와 마찬가지로 a forall
로 묶인 유형 변수 는 한정된 표현식 내에서만 범위에 있습니다.
Post scriptum : 아마도 우리는 타입 매개 변수를 취하는 함수에 대해 생각하고 있다고 생각할 수 있습니다. 왜 우리는 타입 매개 변수에 넣는 것보다 그 매개 변수로 더 흥미로운 것을 할 수 없습니까? 대답은 우리가 할 수 있다는 것입니다!
유형 변수를 레이블과 함께 넣고 새로운 유형을 반환하는 함수는 유형 생성자 이며 다음과 같이 작성할 수 있습니다.
Either = /\a b -> ...
그러나 이와 같은 유형이 작성되는 방식 Either a b
은 이미 ” Either
이러한 매개 변수에 함수 를 적용 함”을 암시 하기 때문에 완전히 새로운 표기법이 필요합니다 .
반면에, 유형 매개 변수에서 “패턴 일치”의 종류가 다른 유형에 대해 다른 값을 리턴하는 함수는 유형 클래스 의 메소드입니다 . /\
위의 구문 을 약간 확장하면 다음과 같이 제안됩니다.
fmap = /\ f a b -> case f of
Maybe -> (\g x -> case x of
Just y -> Just b g y
Nothing -> Nothing b) :: (a -> b) -> Maybe a -> Maybe b
[] -> (\g x -> case x of
(y:ys) -> g y : fmap [] a b g ys
[] -> [] b) :: (a -> b) -> [a] -> [b]
개인적으로, 나는 Haskell의 실제 구문을 선호한다고 생각합니다 …
유형 매개 변수를 “패턴 일치”하고 임의의 기존 유형을 리턴하는 함수 는 유형 패밀리 또는 기능적 종속성입니다 . 전자의 경우 이미 함수 정의와 매우 유사합니다.
답변
다음은 이미 잘 알고있을 것입니다.
이 forall
키워드는 실제로 Haskell에서 한 가지 방식으로 만 사용됩니다. 당신이 그것을 볼 때 항상 같은 것을 의미합니다.
범용 정량
보편적 정량 타입 형태의 유형이다 forall a. f a
. 해당 유형의 값은 다음과 같이 생각할 수있다 기능 소요 유형을 a
인수로하고, 리턴 값 유형을 f a
. Haskell에서 이러한 형식 인수는 형식 시스템에 의해 암시 적으로 전달됩니다. 이 “함수”는받는 유형에 관계없이 동일한 값을 제공해야합니다. 따라서 값은 다형성입니다. 입니다.
예를 들어 type을 고려하십시오 forall a. [a]
. 해당 유형의 값은 다른 유형 a
을 사용하여 동일한 유형의 요소 목록을 제공합니다 a
. 물론 가능한 구현은 하나뿐입니다. 빈 목록을 제공해야하기 때문에a
절대적으로 모든 유형이 될 수 있으므로 . 빈 목록은 요소 유형이 없기 때문에 요소 유형에서 다형성 인 유일한 목록 값입니다.
또는 유형 forall a. a -> a
입니다. 이러한 함수의 호출자는 type a
과 type 값을 모두 제공합니다 a
. 그런 다음 구현시 동일한 유형의 값을 반환해야합니다 a
. 다시 한 가지 가능한 구현이 있습니다. 주어진 값과 동일한 값을 반환해야합니다.
기존 정량
존재 적 정량화 유형의 양식을 것 exists a. f a
하스켈 그 표기법을 지원하는 경우. 해당 유형의 값으로 간주 될 수있는 한 쌍 (또는 “제품”) 형태로 이루어진 a
입력 값 f a
.
예를 들어 type의 값이 있으면 exists a. [a]
일부 유형의 요소 목록이 있습니다. 어떤 유형이든 될 수 있지만 그것이 무엇인지 모르더라도 그러한 목록에 대해 할 수있는 일이 많이 있습니다. 반대로 되돌 리거나 요소 수를 세거나 요소 유형에 의존하지 않는 다른 목록 작업을 수행 할 수 있습니다.
좋아, 잠깐만 기다려 Haskell forall
이 다음과 같은 “존재”유형을 나타내는 데 사용 하는 이유는 무엇 입니까?
data ShowBox = forall s. Show s => SB s
혼란 스러울 수 있지만 실제로 데이터 생성자 의 유형을 설명하고 있습니다 SB
.
SB :: forall s. Show s => s -> ShowBox
일단 구성되면 유형의 가치 ShowBox
는 두 가지로 구성되는 것으로 생각할 수 있습니다 . type s
값과 함께 유형 s
입니다. 다시 말해서, 그것은 실재적으로 정량화 된 유형의 값입니다. Haskell이 해당 표기법을 지원하면 ShowBox
실제로로 쓸 수 있습니다 exists s. Show s => s
.
runST
그리고 친구들
주어진 점에서 이것들은 어떻게 다릅니 까?
foo :: (forall a. a -> a) -> (Char,Bool)
bar :: forall a. ((a -> a) -> (Char, Bool))
먼저 봅시다 bar
. 유형 a
과 유형 의 함수를 사용하여 유형 a -> a
의 값을 생성합니다 (Char, Bool)
. 예를 들어 Int
로 선택 하여 a
유형의 기능을 제공 할 수 있습니다 Int -> Int
. 그러나 foo
다릅니다. 구현하려면 foo
원하는 유형을 함수에 전달할 수 있어야합니다. 우리가 합리적으로 줄 수있는 유일한 기능은id
입니다.
이제 다음 유형의 의미를 다룰 수 있습니다 runST
.
runST :: forall a. (forall s. ST s a) -> a
따라서 어떤 유형으로 제공하든 runST
유형의 값을 생성 할 수 있어야합니다 . 그렇게하기 위해 반드시 형식 을 사용하는 인수를 사용 합니다 . 또한 구현 유형이로 결정한 유형에 관계없이 유형 값을 생성 할 수 있어야합니다 .a
a
forall s. ST s a
a
a
runST
s
그래, 뭐? 이점은 runST
유형이 유형 a
을 전혀 포함 할 수 없다는 점에서 호출자에게 제한이 있다는 s
것입니다. ST s [s]
예를 들어 type의 값을 전달할 수 없습니다 . 실제로 의미하는 것은의 구현 runST
은 type 값으로 자유롭게 돌연변이를 수행 할 수 있다는 것입니다 s
. 이 유형은이 돌연변이가의 구현에 국한됨을 보증합니다 runST
.
유형은 runST
(A)의 예는 랭크 2 다형성 형태 인수의 유형이 포함되어 있으므로 forall
정량화한다. foo
위 의 유형 은 또한 순위 2입니다.의 유형과 같은 일반적인 다형성 유형 bar
은 순위 -1이지만 인수 유형이 자체 forall
수량화 와 함께 다형성이어야하는 경우 순위 -2가됩니다 . 그리고 함수가 순위 2 인수를 취하면 그 유형은 순위 3 등입니다. 일반적으로 rank의 다형성 인수를 취하는 유형 n
은 rank n + 1
입니다.
답변
누구나 전문 용어에 가파른 수학 자라고 가정하지 않는 명확하고 평범한 영어로 forall 키워드를 완전히 설명 할 수 있습니까?
forall
하스켈과 그 유형 시스템의 맥락에서 그 의미와 적용을 설명하려고 노력할 것 입니다.
그러나 당신이 Runar Bjarnason의 ” 제한적 해방, 자유 제약 제약 ” 이라는 제목의 매우 접근하기 쉽고 좋은 강연으로 안내하고 싶다는 것을 이해하기 전에 . 이 이야기는 실제 문장을 뒷받침하는 스칼라의 사례뿐만 아니라 실제 사용 사례의 사례로 가득 차 forall
있습니다. forall
아래 의 관점 을 설명하려고 노력할 것 입니다.
CONSTRAINTS LIBERATE, LIBERTIES CONSTRAIN
다음 설명을 진행하기 위해이 진술을 요약하고 믿는 것이 매우 중요하므로 대화를 볼 것을 촉구합니다 (적어도 그 일부).
Haskell 타입 시스템의 표현성을 보여주는 매우 일반적인 예는 다음과 같습니다.
foo :: a -> a
이 타입 시그니처가 주어지면,이 타입을 만족시킬 수있는 함수는 하나 뿐이며 그 identity
함수 또는 더 널리 알려진 함수라고합니다id
합니다.
Haskell을 배우는 시작 단계에서 나는 항상 아래 기능을 궁금해했습니다.
foo 5 = 6
foo True = False
그들은 위의 형식 서명을 모두 만족시킵니다. 그렇다면 Haskell 사람들은 왜 그것이 id
은 형식 서명을 만족시키는 단독 합니까?
forall
형식 서명에 숨겨진 암시가 있기 때문입니다 . 실제 유형은 다음과 같습니다.
id :: forall a. a -> a
이제 진술로 돌아 갑시다. 제약은 해방하고 자유는 구속합니다
이것을 유형 시스템으로 변환하면 다음 문장이됩니다.
유형 수준의 제약은 용어 수준에서 자유가 됨
과
유형 수준의 자유는 용어 수준의 제약이됩니다.
첫 번째 진술을 증명하려고 노력합시다.
유형 수준의 제약 ..
타입 시그니처에 제약을두기
foo :: (Num a) => a -> a
용어 수준
에서 자유가 됨 우리에게이 모든 것을 쓸 수있는 자유 또는 유연성을 준다
foo 5 = 6
foo 4 = 2
foo 7 = 9
...
a
다른 타입 클래스 등 으로 제한 해도 마찬가지입니다.
이제이 유형 서명 foo :: (Num a) => a -> a
은 다음과 같이 변환됩니다.
∃a , st a -> a, ∀a ∈ Num
이것은에 변환 존재 정량화로 알려져있다 존재 의 일부 인스턴스 a
유형의 무언가를 공급하는 기능에 대한a
가 동일한 유형의 무언가를 반환 하고 해당 인스턴스는 모두 숫자 세트에 속한다는 것을 의미합니다.
따라서 우리는 제약 조건 ( a
숫자 집합에 속해야 함)을 추가하고 여러 수준의 구현을 가질 수 있도록 용어 수준을 해제합니다.
이제 두 번째 진술과 실제로 다음과 같은 설명을 수행합니다 forall
.
유형 수준의 자유는 용어 수준의 제약이됩니다.
이제 타입 레벨에서 함수를 해방하자 :
foo :: forall a. a -> a
이제 이것은 다음과 같이 번역됩니다.
∀a , a -> a
즉,이 유형 서명의 구현은 a -> a
모든 상황에 적합 해야합니다 .
이제 이것은 용어 수준에서 우리를 구속하기 시작합니다. 더 이상 쓸 수 없습니다
foo 5 = 7
우리가 넣을 경우이 구현은 만족하지 않기 때문에 a
A와 Bool
. a
a Char
또는 a [Char]
또는 사용자 정의 데이터 유형일 수 있습니다. 모든 상황에서 비슷한 유형의 것을 반환해야합니다. 유형 수준에서의 자유는 보편적 정량화로 알려져 있으며 이것을 충족시킬 수있는 유일한 기능은
foo a = a
일반적으로 identity
함수 라고 합니다
따라서, forall
A는 liberty
실제의 목적이다 형 수준에서 constrain
특정 구현 용어 레벨.
답변
이 키워드가 다른 용도로 사용되는 이유는 키워드가 상위 유형 및 실존성이라는 두 가지 이상의 다른 유형 시스템 확장에서 실제로 사용되기 때문입니다.
왜 ‘forall’이 동시에 적절한 구문 비트인지에 대한 설명을 얻는 것보다는이 두 가지를 개별적으로 읽고 이해하는 것이 가장 좋습니다.