haskell 유형 변수에 부등식 제약 조건을 둘 수 있습니까?

Question

함수의 형식 변수에 부등식 제약 조건을 적용 할 수 있습니까? foo :: (a ~ b) => a -> bGHC type family docs 같이 같음이 아닌 다른 수식 제외?

ghc 문서가 내 지식을 나열하지 않기 때문에 가능한 직접적인 방법이 없다는 것을 알고 있습니다. 그러나 이것이 모든면에서 가능하지 않다면 나는 거의 당황 할 것입니다. 나는 이국적인 타입 - fu에 노출되었다.

Answer 1

우선, 고유 한 유형 변수가 해당 범위 내에서 이미 통합 할 수 없음을 기억하십시오. 예를 들어, \x y -> x 인 경우 유형 기호 a -> b -> c을 지정하면 고정 유형 변수와 일치하지 못하는 것에 대한 오류가 발생합니다. 따라서이 함수는 함수를 호출하는 모든 항목에만 적용되며 두 가지 유형을 동일하게 만드는 간단한 다형 함수를 사용하지 못하게합니다. 그것은 이런 식으로 뭔가를 작동합니다, 나는 가정 개인적으로

const' :: (a ~/~ b) => a -> b -> a 
const' x _ = x 

foo :: Bool 
foo = const' True False -- this would be a type error 

나는이 정말 유용 할 것이다 의심 - 유형 변수의 독립성은 이미 사소한 일에 무너 두 가지 유형을 알고에서 일반적인 기능을 방지 동일하지 않습니다하지 실제로 당신이 흥미로운 것을 할 수있게합니다 (평등과는 달리, 두 가지 유형을 강요하게합니다). 조건부가 아니라 선언적이라는 것은 일종의 전문화 기술의 일부로 평등/불평등을 구분할 수 없다는 것을 의미합니다 .

그래서 내가 원하는 곳에서 특정 용도로 사용한다면 다른 접근 방법을 시도해 보시기 바랍니다. 한편

, 당신은 그냥 말도 안되는 타입 해커와 재생하려면 ...

{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE UndecidableInstances #-} 
{-# LANGUAGE OverlappingInstances #-} 

-- The following code is my own hacked modifications to Oleg's original TypeEq. Note 
-- that his TypeCast class is no longer needed, being basically equivalent to ~. 

data Yes = Yes deriving (Show) 
data No = No deriving (Show) 

class (TypeEq x y No) => (:/~) x y 
instance (TypeEq x y No) => (:/~) x y 

class (TypeEq'() x y b) => TypeEq x y b where 
    typeEq :: x -> y -> b 
    maybeCast :: x -> Maybe y 

instance (TypeEq'() x y b) => TypeEq x y b where 
    typeEq x y = typeEq'() x y 
    maybeCast x = maybeCast'() x 

class TypeEq' q x y b | q x y -> b where 
    typeEq' :: q -> x -> y -> b 
    maybeCast' :: q -> x -> Maybe y 

instance (b ~ Yes) => TypeEq'() x x b where 
    typeEq'() _ _ = Yes 
    maybeCast' _ x = Just x 

instance (b ~ No) => TypeEq' q x y b where 
    typeEq' _ _ _ = No 
    maybeCast' _ _ = Nothing 

const' :: (a :/~ b) => a -> b -> a 
const' x _ = x 

글쎄, 그건 믿을 수 없을만큼 바보였다. 그래도 작동합니다.

> const' True() 
True 
> const' True False 

<interactive>:0:1: 
    Couldn't match type `No' with `Yes' 
    (...) 

Answer 2

GHC 7.8.1. closed type families are available. 해결책은 그 (것)들로 매우 더 간단하다 :

data True 
data False 

type family TypeEqF a b where 
    TypeEqF a a = True 
    TypeEqF a b = False 

type TypeNeq a b = TypeEqF a b ~ False