는 지금까지 내가 그것을 다른 말로, 무료 정리를 약화 또는 때문에 다형성 seq 기능이 나쁜 알고, seq없이 유효 몇 가지 등식은 더 이상 유효하지 seq에 없습니다 . 예를 들어, 평등
map g (f xs) = f (map g xs)
모든 기능 g :: tau -> tau', 모든 목록 xs :: [tau] 모든 다형성 기능 f :: [a] -> [a]을 위해 보유하고 있습니다. 기본적으로이 평등은 f이 인수 목록의 요소를 다시 정렬하거나 요소를 삭제하거나 복제 할 수 있지만 새 요소를 만들 수는 없다고 명시합니다.
솔직하게 말하면, 오류의 유형이 다형성이므로 종료되지 않는 계산/런타임 오류를 목록에 "삽입"할 수 있기 때문에 요소를 만들 수 있습니다. 즉,이 평등은 이미 하스켈 같은 프로그래밍 언어로 깨져있다. seq이 없다. 다음 함수 정의는 방정식에 대한 반례를 제공합니다. 기본적으로 왼쪽의 g은 오류를 "숨 깁니다". 방정식을 해결하기 위하여
g _ = True
f _ = [undefined]
는 g는 오류에 오류를 매핑한다, 즉, 엄격한이어야한다. 이 경우 평등이 다시 유지됩니다.
다형성 seq 연산자를 추가하면 방정식이 다시 중단됩니다. 예를 들어 다음 인스턴스 생성은 카운터 예제입니다.
g True = True
f (x:y:_) = [seq x y]
우리가 목록 xs = [False, True]을 고려하면, 우리는 다른 한편으로
f (map g [False, True]) = f [undefined, True] = [undefined]
에, 당신이 특정의 요소를 만들기 위해 seq를 사용할 수
map g (f [False, True]) = map g [True] = [True]
을 가지고 있지만 목록의 위치는 목록의 다른 요소의 정의에 따라 다릅니다. g이 합계 인 경우 동등 함이 다시 유지됩니다.무료 theorems에서 intereseted 경우 seq와 함께 오류가있는 언어를 고려하고 있는지 언어를 고려하고 있는지 지정할 수있는 free theorem generator을 확인하십시오. 이 기능이 덜 실용적인 것처럼 보일 수도 있지만 seq은 기능 프로그램의 성능을 향상시키는 데 사용되는 일부 변환을 중단합니다. 예를 들어 seq이있는 경우 foldr/build 융합이 실패합니다. seq이있는 상태에서 무료 정리에 대한 자세한 내용을 알아 보려면 Free Theorems in the Presence of seq을 살펴보십시오.
내가 알고있는 한, 다형성 seq은 특정 변형이 언어에 추가되었을 때 깨졌습니다. 그러나 알타이 산들 역시 단점을 가지고있다. seq을 기반으로 한 유형 클래스를 추가하는 경우 seq을 깊이 깊이 추가하면 프로그램에 유형 클래스 제약 조건을 많이 추가해야 할 수 있습니다. 또한 seq을 사용하여 수정 될 수있는 공간 누수가 있다는 것을 이미 알고 있었기 때문에 seq을 생략하는 것은 선택 사항이 아니 었습니다.
마지막으로, 나는 뭔가를 놓칠지도 모르지만 seq 연산자가 a -> a 일하는 방식을 알지 못합니다. seq의 단서는 다른 표현식이 정상 형식으로 향하는 것으로 평가되는 경우 정규 표현식으로 향하는 표현식을 평가한다는 것입니다. seq 유형이 a -> a 인 경우 하나의 표현식을 다른 표현식의 평가에 따라 평가할 수있는 방법이 없습니다.
'seq' 함수는 람다 정의 가능하지 않습니다 (i.r., 람다 계산법에서 정의 할 수 없습니다). 즉,'seq'가있을 때 람다 미적분의 모든 결과를 더 이상 신뢰할 수 없다는 것을 의미합니다. – augustss