TypeApplicationsとAllowAmbiguousTypes

Overlapping Instances

• Avoid overlapping instances with closed type families

OverlappingInstanceは非常に便利なのだけど、外部モジュールでインスタンス追加されて変なことが起こることがあるから、回避したくなることがある。そのトリックの一つ、ということなのだけどProxy使っているので最近追加されたTypeApplicationsでProxy消したいと思った次第。できた。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

type family (F a) :: Bool where
    F Char  = 'True
    F Bool  = 'True
    F a     = 'False

class ShowList a where
    showl :: [a] -> String

instance (ShowList' (F a) a) => ShowList a where
    showl = showl' @(F a) @a

class ShowList' (flag :: Bool) a where
    showl' :: [a] -> String

instance ShowList' 'True Char where
    showl' str = str

instance ShowList' 'True Bool where
    showl' ls = map (\b -> if b then '1' else '0') ls

instance (Show a) => ShowList' 'False a where
    showl' x = show x

main = do
    -- 型毎にちゃんと別々のインスタンスが選ばれる
    putStrLn $ showl "abc"
    putStrLn $ showl [True, False, True]
    putStrLn $ showl @Int [1, 2, 3]

追加したプラグマはTypeApplications(ghc-8.0.1から), AllowAmbiguousTypes(ghc-7.8.1から)の二つ。
後者はクラス定義時の制約を緩められるものらしく、付けないと

test.hs:23:5: error:
    • Could not deduce (ShowList' flag0 a)
      from the context: ShowList' flag a
        bound by the type signature for:
                   showl' :: ShowList' flag a => [a] -> String
        at test.hs:23:5-27
      The type variable ‘flag0’ is ambiguous
    • In the ambiguity check for ‘showl'’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        showl' :: forall (flag :: Bool) a.
                  ShowList' flag a =>
                  [a] -> String
      In the class declaration for ‘ShowList'’

というように怒られる。確かにShowList'をみると、

class ShowList' (flag :: Bool) a where
    showl' :: [a] -> String

showl'を呼んでも引数や返り値の型からflag :: Boolが一意に決まらない。その曖昧性を許容して、call sitesまで遅らせる拡張がAllowAmbiguousTypesらしい。
現在はTypeApplicationsがあるため、引数にProxyで無理やり型情報持たせなくても簡単に型を指定できるようになった。便利だ。
showl'の呼び出し箇所は以下だ。

instance (ShowList' (F a) a) => ShowList a where
    showl = showl' @(F a) @a

@を用いて型をshowl'に渡している。showl'の正確な型は、

showl' :: forall (flag :: Bool) a.
         ShowList' flag a =>
         [a] -> String

であるため、forallに記述されているflagとaを、呼び出し側で@で渡せば良い。
そうするとflag :: Boolも一意に決まり、問題はなくなったということだ。Ambiguousという名称から曖昧性を最後まで残すことを許容するのか?と思ったがそういうことではないようだ。

ところで

OverlappingInstances回避のためにUndecidableInstances突っ込んでしまうのはよくないような...これはtypeCheckerが止まらなくなる可能性がある非常に危険な拡張だ。ということでそれも消せないか少し試してみたがうまくいかなかった。
OverlapInstancesはモジュールを跨いだ問題なのに対しUndecidableInstancesの影響はモジュール内で完結する(本当か?)からトレードオフとしては有りなのかな。

ところで2

AllowAmbiguousTypesが必要なところでは引数や返り値から型変数を決定できなくなるわけだから、当然型推論が効かなくなるのだな。
こういうtypecheckerがinstance決定時に必ず止まるための制約とか「型推論がなるべく効くための制約」がghcには結構存在して、それを外すための拡張がそれぞれ存在していたりする。それぞれの制約はUserGuide等に書いてあることも多いが、ユーザからしたら一見不合理な制約に見えてしまうのだな。