Haskell: поощрение GHC к выводу правильного промежуточного типа - PullRequest
Новая
       27

Haskell: поощрение GHC к выводу правильного промежуточного типа

7 голосов
/ 19 февраля 2012

Я подумал, что было бы неплохо разрешить произвольное цепное сравнение в Haskell, поэтому вы могли бы делать простые проверки диапазона, такие как: 

x <= y < z

и более сложные вещи, такие как 

x /= y < z == a

Где два вышеупомянутых семантически эквивалентны 

x <= y && y < z
x /= y && y < z && z == a

Просто посмотреть, смогу ли я заставить синтаксис работать.

Так что я проделал большую часть пути, используя пару классов типов: 

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module ChainedOrd where

import Prelude hiding ((<), (<=), (>), (>=), (==), (/=))

class Booly v a where
  truthy :: v -> a
  falsy :: v -> a

instance Booly a Bool where
  truthy = const True
  falsy = const False

instance Booly a (Maybe a) where
  truthy = Just
  falsy = const Nothing

class ChainedOrd a b where
  (<),(>),(<=),(>=),(==),(/=) :: (Booly b c) => a -> b -> c

infixl 4 <
infixl 4 >
infixl 4 <=
infixl 4 >=
infixl 4 ==
infixl 4 /=

instance Ord a => ChainedOrd a a where
  x < y     = case compare x y of LT -> truthy y ; _ -> falsy y
  x > y     = case compare x y of GT -> truthy y ; _ -> falsy y
  x <= y    = case compare x y of GT -> falsy y  ; _ -> truthy y
  x >= y    = case compare x y of LT -> falsy y  ; _ -> truthy y
  x == y    = case compare x y of EQ -> truthy y ; _ -> falsy y
  x /= y    = case compare x y of EQ -> falsy y  ; _ -> truthy y

instance Ord a => ChainedOrd (Maybe a) a where
  Just x < y     = case compare x y of LT -> truthy y ; _ -> falsy y
  Nothing < y    = falsy y
  Just x > y     = case compare x y of GT -> truthy y ; _ -> falsy y
  Nothing > y    = falsy y
  Just x <= y    = case compare x y of GT -> falsy y  ; _ -> truthy y
  Nothing <= y   = falsy y
  Just x >= y    = case compare x y of LT -> falsy y  ; _ -> truthy y
  Nothing >= y   = falsy y
  Just x == y    = case compare x y of EQ -> truthy y ; _ -> falsy y
  Nothing == y   = falsy y
  Just x /= y    = case compare x y of EQ -> falsy y  ; _ -> truthy y
  Nothing /= y   = falsy y

Который прекрасно компилируется, но, похоже, не позволяет создавать цепочки из-за проблемы промежуточных типов. 

-- works
checkRange1 :: Ord a => a -> a -> a -> Bool
checkRange1 x y z = x `lem` y <= z
  where lem :: Ord a => a -> a -> Maybe a
        lem = (<=)

-- works
checkRange2 :: Ord a => a -> a -> a -> Bool
checkRange2 x y z = (x <= y) `leb` z
  where leb :: Ord a => Maybe a -> a -> Bool
        leb = (<=)

checkRange1 и checkRange2 работают нормально, так какоба они накладывают ограничение на промежуточный тип (либо в результате первого сравнения, либо в качестве аргумента для второго). 

-- error
checkRange3 :: Ord a => a -> a -> a -> Bool
checkRange3 x y z = (x <= y) <= z

Когда я пытаюсь позволить компилятору выводить промежуточный тип, хотя, он лает на меня. 

ChainedOrd.hs:64:30:
    Ambiguous type variable `a0' in the constraints:
      (ChainedOrd a0 a) arising from a use of `<='
                        at ChainedOrd.hs:64:30-31
      (Booly a a0) arising from a use of `<=' at ChainedOrd.hs:64:24-25
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: (x <= y) <= z
    In an equation for `checkRange3': checkRange3 x y z = (x <= y) <= z

Есть ли способ убедить компилятор, что он должен использовать Maybe a в качестве промежуточного типа a0, удовлетворяющий Booly a a0, ChainedOrd a0 a, поскольку это единственный экземпляр, который он знаето?

Failingчто, есть ли другой способ сделать работу цепочки произвольного сравнения?

Ответы [ 4 ]

5 голосов
/ 19 февраля 2012 
infixl 4 ==?

class ChainedEq a b where
  (==?) :: a -> b -> Maybe b

instance (Eq a) => ChainedEq (Maybe a) a where
  x ==? y = if x == Just y
    then x
    else Nothing

instance (Eq a) => ChainedEq a a where
  x ==? y = if x == y
    then Just x
    else Nothing

unChain :: Maybe a -> Bool
unChain Nothing = False
unChain (Just _) = True

test :: Int -> Int -> Int -> Bool
test x y z = unChain $ x ==? y ==? z
4 голосов
/ 19 февраля 2012

Есть способы сообщить компилятору, какой тип использовать: 

checkRange4 x y z = ((x <= y) `asTypeOf` Just x) <= z

или вы можете использовать ScopedTypeVariables, перевести переменную типа в область действия и поставить сигнатуру типа на x <= y.Но вы не можете сказать компилятору использовать только те экземпляры, о которых он знает.Компилятор работает в предположении открытого мира, могут быть определены другие экземпляры, и код должен работать, если они есть и входят в область видимости.Поэтому все, что вы делаете, будет более неуклюжим, чем 

checkRange5 x y z = x <= y && y <= z
3 голосов
/ 20 февраля 2012

Вот как бы я это сделал: 

{-# LANGUAGE NoMonomorphismRestriction #-}

data Chain v e = Link { evaluation :: e
                      , val :: v
                      , next :: Chain v e
                      }
               | Start { val :: v }


liftChain :: (a -> a -> b) -> Chain a b -> a -> Chain a b
liftChain f ch x = Link { evaluation = val ch `f` x, val = x, next = ch }

(.<)  = liftChain (<)
(.>)  = liftChain (>)
(.<=) = liftChain (<=)
(.>=) = liftChain (>=)
(.==) = liftChain (==)

toList :: Chain v e -> [v]
toList (Start v) = [v]
toList (Link _ v n) = v : toList n

toList' :: Chain v e -> [e]
toList' (Start _) = []
toList' (Link e _ n) = e : toList' n

and' :: Chain v Bool -> Bool
and' = and . toList'

Использование: 

ghci> and' $ Start 3 .< 4 .< 7 .== 7 .< 9 .>= 0 .== (2-2)
True
1 голос
/ 20 февраля 2012

Мне не давало покоя, что это не могло бы казаться выразительным без неуклюжих функций завершения / распаковки.То, что я придумал, чтобы разрешить чисто инфиксные выражения: 

{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE TypeFamilies              #-}

module ChainedComp where

infixl 4 ==.. , .==. , ==?

data Comp1Chain a = Sofar1OK a | Already1Failed
data Comp2Chain a = Sofar2OK a | Already2Failed
data Comp3Chain a = Sofar3OK a | Already3Failed
-- ...

(==..) :: (Eq a) => a -> a -> Comp1Chain a
x==..y | x==y       = Sofar1OK y
       | otherwise  = Already1Failed

class ChainableComp c where
  type AppendElem c :: *
  type ChainAfterAppend c :: *
  (.==.) :: c -> AppendElem c -> ChainAfterAppend c
  (==?) :: c -> AppendElem c -> Bool


instance (Eq a) => ChainableComp (Comp1Chain a) where
  type AppendElem (Comp1Chain a) = a
  type ChainAfterAppend (Comp1Chain a) = Comp2Chain a
  chn.==.y | (Sofar1OK x)<-chn, x==y  = Sofar2OK x
           | otherwise                = Already2Failed
  chn==?y | (Sofar1OK x)<-chn, x==y  = True
          | otherwise                = False
instance (Eq a) => ChainableComp (Comp2Chain a) where
  type AppendElem (Comp2Chain a) = a
  type ChainAfterAppend (Comp2Chain a) = Comp3Chain a
  chn.==.y | (Sofar2OK x)<-chn, x==y  = Sofar3OK x
           | otherwise                = Already3Failed
  chn==?y | (Sofar2OK x)<-chn, x==y  = True
          | otherwise                = False
-- ...

И с этим вы можете написать 

*ChainedComp> 7 ==..7.==.7==? 7
True
*ChainedComp> 7 ==..7.==.6==? 7
False
*ChainedComp> 5 ==..5.==.5.==.4.==.5.==.5==? 5
False

Не совсем красиво, но IMO лучше читаетсядругие решения.Количество необходимых объявлений экземпляров, конечно, не так приятно, но раз и навсегда, так что я полагаю, это не так уж и плохо.

...