왜 하스켈은 Eq의 강력한 대안을 가지고 있지 않습니까?

Question

Set이 functor가 아닌 이유는 here입니다. a == b && f a /= f b이 가능하다는 사실로 요약됩니다. 그럼, 왜하는 경우는 법률

∀a,b,f. not (a === b) || (f a === f b) 
∀a. a === a 
∀a,b. (a === b) == (b === a) 

어쩌면 약간 다른 사람을 순종하기로되어 있으며, 표준으로

class Eq a => StrongEq a where 
    (===) :: a -> a -> Bool 
    (/==) :: a -> a -> Bool 
    x /== y = not (x === y) 
    x === y = not (x /== y) 

같은 것을 식의 대안을 하스켈하지 않는 이유는 무엇입니까? 그러면 우리는 다음을 가질 수 있습니다 :

instance StrongEq a => Functor (Set a) where 
    -- ... 

또는 뭔가 빠졌습니까?

---

편집 : 내 문제는? "왜 Eq 예를없이 종류가 있습니다"당신의 일부가 대답 한 것처럼되지 않습니다. 그것은 반대입니다 : "왜 연장적으로 동일하지 않은 Eq의 인스턴스가 있습니까? Eq 인스턴스가 너무 많은 이유는 무엇입니까? "a == b이 확장 항등을 암시하는 경우 이 (가) Functor의 인스턴스가 아닌 이유는 무엇입니까?"

또한 내 인스턴스 선언은 쓰레기 (thanks @ n.m.)입니다. 나는 말했다해야합니다

이

newtype StrongSet a = StrongSet (Set a) 
instance Functor StrongSet where 
    fmap :: (StrongEq a, StrongEq b) => (a -> b) -> StrongSet a -> StrongSet b 
    fmap (StrongSet s) = StrongSet (map s) 

Answer 1

두 번째 Functor 인스턴스도 의미가 없습니다. Set이 하스켈에서 Functor 일 수없는 가장 큰 이유는 fmap은 제약 조건을 가질 수 없습니다. 평등에 대한 다른 개념을 StrongEq으로 정의하더라도 Set 인스턴스의 fmap에 이러한 제약 조건을 쓸 수 없다는 사실은 변하지 않습니다.

fmap 일반적으로 은 (는)에 제약 조건이 없어야합니다. 예를 들어 Functor 내부에 기능을 적용하기 위해 Applicative를 사용하는 개념이 전혀 없으면 함수의 펑터를 얻는 것이 합리적입니다. 함수는 일반적으로 Eq 또는 StrongEq의 멤버가 될 수 없습니다.

fmap 때문에 같은 코드로, 일부 경우에 별도의 제약이 없습니다

이 코드는 펑 f 및 g에 관계없이 작동 주장

,에 관계없이 기능 h 및 j의

fmapBoth :: (Functor f, Functor g) => (a -> b, c -> d) -> (f a, g c) -> (f b, g d) 
fmapBoth (h, j) (x, y) = (fmap h x, fmap j y) 

. 펑터 중 하나가 fmap에 대한 추가 제약 조건을 가진 특수한 것인지 여부를 확인하는 방법이 없으며 적용 대상 함수 중 하나가 이러한 제약 조건을 위반하는지 여부를 확인하는 방법도 없습니다.

세트가 하스켈의 Functor라고 말하면, 정확한 타입의 (fmap :: (a -> b) -> Set a -> Set b) 합법적 인 작업이 있다고 말합니다. 즉 정확히 무엇 Functor 의미합니다. fmap :: (Eq a -> Eq b) => (a -> b) -> Set a -> Set b은 그러한 작업의 예가 아닙니다.

그것은 내가은 Functor에 따라 다를 값에 대한 제한을 허용하는 다른 펑터 클래스를 작성하기 위해 ConstraintKinds GHC extendsion을 사용, 이해 가능하다 (그리고 당신이 실제로 필요한 것은 단지 Eq, Ord 제약이다). This blog post은 Set에 대한 인스턴스를 가질 수있는 새로운 Monad 클래스를 만들기 위해 그렇게하는 것에 대해 이야기합니다. 이런 코드로 놀아 본 적이 없기 때문에이 기술이 있다는 것만 알면됩니다. Functors가 필요한 기존 코드로 Sets를 넘기는 것을 돕지는 않지만 원한다면 Functor 대신 사용할 수 있어야합니다.

Answer 2

instance StrongEq a => Functor (Set a) where 

이에 상관없이 어떤 StrongEq 수단, 하스켈이나 사물의 그랜드 수학/범주 체계로도 의미가 있습니다.

하스켈에서 Functor에는 종류가 * -> * 인 유형 생성자가 필요합니다. 화살표는 범주 이론에서 펑터가 일종의 매핑이라는 사실을 반영합니다. [] 및 (가상의) Set은 이러한 유형 생성자입니다. [a] 및 Set a은 종류가 *이며 펑터가 될 수 없습니다.

하스켈에서는 Functor으로 지정할 수 있도록 Set을 정의하기가 어렵습니다. 왜냐하면 어떤 유형에 대해서도 평등을 현명하게 정의 할 수 없기 때문입니다. 예를 들어, Integer->Integer 유형의 두 가지를 비교할 수 없습니다.

는 이제

goedel :: Integer -> Integer -> Integer 
goedel x y = -- compute the result of a function with 
      -- Goedel number x, applied to y 

당신이 값 s :: Set Integer가 있다고 가정하는 기능이있는 가정하자. fmap goedel s은 어떻게 생겼습니까? 중복을 어떻게 제거합니까?

평범한 세트 이론에서는 함수를 포함하여 모든 것이 평등하게 정의되므로 Set (또는 정확하게는 Powerset)이 재미입니다. 문제는 없습니다.

Answer 3

이 개념은 StrongEq입니다. 일반적으로 평등은 컴퓨터 과학이 일을 어렵게 만드는 방식으로 전형적인 수학보다 훨씬 엄격 해지는 곳입니다.

특히 일반적인 수학은 객체가 집합에 존재하는 것처럼 말하고 고유하게 식별 될 수 있습니다.컴퓨터 프로그램은 대개 항상 계산할 수없는 유형을 처리합니다 (간단한 반례로 data U = U (U -> U) 유형에 해당하는 집합이 무엇인지 알려주십시오). 즉, 두 개의 값을 식별 할 수 있는지 여부를 결정할 수 없습니다.

typechecking은 같은 유형을 식별해야하며 의존적으로 형식화 된 언어는 유형에 임의의 값을 가질 수 있으므로 동등성을 표현할 방법이 필요하기 때문에 의존적으로 입력 된 언어에서는 막대한 주제가됩니다.

따라서, 평등을 위해 결정적으로 비교할 수있는 유형 만 포함하는 Haskell의 제한된 부분에 대해 StrongEq을 정의 할 수 있습니다. 우리는 이것을 화살표로 계산 가능한 함수로 간주 할 수 있고 유형에서 유형의 값 집합 유형에 이르기까지 endofunctor로 Set을 볼 수 있습니다. 불행히도, 이러한 제한은 Haskell 표준에서 멀리 떨어져 있으며, StrongEq 또는 Functor (Set a)을 실용적이지 못하게 정의합니다.

Answer 4

내가 범주 이론가 아니에요 때문에, 내가 좀 더 구체적인/실제적인 설명을 작성하려고합니다 (즉, 하나는 내가 이해할 수) :

중요한 점은 만들어 @leftaroundabout 하나입니다 즉 반드시 동일한 구현 만 보유해야 a == b을 필요로하지 않습니다 (

==는 "모든 관찰에 의해 해당" 증거하도록되어 있지만 아무것도 당신은 "공식적으로"a와 b로 할 수있는 : 코멘트 다시 산출해야합니다. equiva 결과를 빌려줬다. 따라서 unAlwaysEq은 첫 번째 장소에 노출되어서는 안됩니다. 일부 유형에 대해이를 보장 할 수 없다면 에 Eq 인스턴스를 입력하지 않아야합니다. 이다

이미 수에 StrongEq 무엇 Eq 예정이다 그건 그 때문에 필요가 없습니다.

하스켈 값은 종종 을 나타내며,은 일종의 수학적 또는 "실생활"값을 나타냅니다. 여러 번,이 표현은 일대일입니다. 예를 들어, 유형을 고려해보십시오.

data PlatonicSolid = Tetrahedron | Cube | 
    Octahedron | Dodecahedron | Icosahedron 

이 유형에는 각 Platonic 솔리드의 표현이 정확히 하나 포함되어 있습니다. 선언문에 deriving Eq을 추가하면이를 활용할 수 있으며 올바른 인스턴스가 생성됩니다.

그러나 많은 경우 동일한 추상 값이 둘 이상의 하스켈 값으로 표시 될 수 있습니다. 예를 들어, 빨강 - 검정 나무 Node B (Node R Leaf 1 Leaf) 2 Leaf 및 Node B Leaf 1 (Node R Leaf 2 Leaf)은 둘 다 세트 {1,2}를 나타낼 수 있습니다. 우리의 선언에 deriving Eq을 추가하면, 우리는 동일하게 간주되기를 바라는 것들을 구별 할 수있는 Eq의 인스턴스를 얻을 것이다 (집합 연산의 구현을 벗어남).

해당하는 경우 유형이 Eq (및 Ord)으로 만 만들어 졌는지 확인하는 것이 중요합니다. Ord의 인스턴스를 만들기 만하면 주문을 필요로하는 데이터 구조에 넣을 수 있습니다.하지만 주문이 실제로 주문의 추상 값이 아니라면 모든 종류의 파손이 발생할 수 있습니다.예를 들어 문서가 절대적으로 보장하지 않는다면 sort :: Ord a => [a] -> [a]이라는 함수는 불안정한 정렬 일뿐만 아니라 그 안에 들어있는 모든 하스켈 값을 포함하는 목록을 생성하지 않을 수도 있습니다. sort [Bad 1 "Bob", Bad 1 "James"]은 [Bad 1 "Bob", Bad 1 "James"], [Bad 1 "James", Bad 1 "Bob"], [Bad 1 "James", Bad 1 "James"] 또는 [Bad 1 "Bob", Bad 1 "Bob"]을 합리적으로 생성 할 수 있습니다. 이들 모두는 완벽하게 합법적입니다. 뒤쪽 방에서 unsafePerformIO을 사용하여 라스베가스 스타일의 무작위 알고리즘을 구현하거나 가장 빠른 속도의 답변을 얻기 위해 서로에 대한 스레드를 경주하는 기능은 서로 == 인 한 다른 결과가 서로 다른 시간을 줄 수도 있습니다 .

tl; dr : 무언가를 Eq으로 설정하는 것은 전 세계에 매우 강력한 성명을 제시하는 방법입니다. 당신이 그것을 의미하지 않는다면 그 진술을하지 마십시오.