用2个函数理解`~`

Question

背景:我不明白〜并且正在请求用例.

鉴于:

{-# LANGUAGE GADTs #-}

f :: a ~ b => a -> b -> b
f a b = a

g :: a -> a -> a
g a b = a

在我看来,两个函数都是相同的:

Prelude> :r
[1 of 1] Compiling Main             ( TypeEq.hs, interpreted )
Ok, modules loaded: Main.
*Main> f 10 20
10
*Main> g 10 20
10

在什么情况下会是使用有用f了g？

Answer 1

{-# LANGUAGE TypeFamilies #-}

import GHC.Exts (IsList(..))

fizzbuzz :: (IsList l, Item l ~ Int) => l -> IO ()
fizzbuzz = go . toList
 where go [] = return ()
       go (n:m)
        | n`mod`3==0  = putStrLn "fizz" >> go m
        | n`mod`5==0  = putStrLn "buzz" >> go m
        | otherwise   = print n >> go m

然后

Prelude> fizzbuzz [1..7]
1
2
fizz
4
buzz
fizz
7
Prelude> import Data.Vector.Unboxed as UA
Prelude UA> fizzbuzz (UA.fromList[1..7] :: UA.Vector Int)
1
2
fizz
4
buzz
fizz
7

您现在可能会反对使用Foldable约束更好地完成此操作,而不是将丑陋的转换为列表.实际上这是无法做到的,因为由于Unbox约束,未装箱的矢量没有可折叠的实例!

然而,它也可以用非等式约束来完成,即

fizzbuzz :: (IsList l, Num (Item l), Eq (Item l), Show (Item l))
     => l -> IO ()

这更为一般,但可以说也更尴尬.实际上,当你需要只有一个包含类型时,一个等式约束可能是一个不错的选择.

实际上,我有时会发现抛出一个等式约束只是为了使类型签名更简洁,如果它有点重复那么方便:签名

complicatedFunction :: Long (Awkward (Type a) (Maybe String))
                 -> [Long (Awkward (Type a) (Maybe String))]
                 -> Either String (Long (Awkward (Type a) (Maybe String)))

可以替换为

complicatedFunction :: r ~ Long (Awkward (Type a) (Maybe String))
             => r -> [r] -> Either String r

这可能比其他干燥的可能性更好

type LAwkTS a = Long (Awkward (Type a) (Maybe String))

complicatedFunction :: LAwkTS a -> [LAwkTS a] -> Either String (LAwkTS a)