overlapping/Incoherent closed type families

I have been playing around a bit with closed type families however I somehow always bump my head at the fact that things usually doesn't work for Num without specifying the type.

Here is an example.

{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE OverlappingInstances      #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
module Main where

import Data.Typeable

type family UnMaybed a where
    UnMaybed (Maybe a) = a
    UnMaybed a = a

class UnMaybe x where
    unMaybe :: x -> UnMaybed x

instance UnMaybe (Maybe a) where
    unMaybe (Just a) = a

instance (UnMaybed a ~ a) => UnMaybe a where
    unMaybe a = a

main = do
    print $ unMaybe 'c'
    print $ unMaybe (1::Int)
    print $ unMaybe (Just 1)
    print $ unMaybe 1 -- this line does not compile

everything except the last line will compile.

../Example.hs:23:17:
    Occurs check: cannot construct the infinite type: s0 ~ UnMaybed s0
    The type variable ‘s0’ is ambiguous
    In the second argument of ‘($)’, namely ‘unMaybe 1’
    In a stmt of a 'do' block: print $ unMaybe 1

Now I know this is because numbers are polymorphic and ( Maybe a ) could be an instance of Num . I think for normal overlapping typeclasses this dilemma can be solved by using the IncoherentInstances PRAGMA. Anyway, I wanted to ask if there is a way to make this work in type families?

I also thought about specifying Num explicitly in UnMaybed

type family UnMaybed a where
    unMaybed (Num a => a) = a
    UnMaybed (Maybe a) = a
    UnMaybed a = a

This compiles but i think the first case will never be matched this is probably a bug.

---

Answer from: http://www.haskell.org/pipermail/haskell-cafe/2014-March/113153.html

This is a limitation of closed type families, but the limitation is there for good reason.

IncoherentInstances threatens coherence of type class instances, meaning that a constraint UnMaybe <<some type>> might be fulfilled differently in different places, even for the same <<some type>> . But, type class instance selection is purely a runtime-behavior effect. Choosing a different instance cannot affect the types in your program.

Type families, on the other hand, directly affect the types. Allowing incoherence like the way IncoherentInstances works could be used to implement unsafeCoerce.

There's not much of a way around it without a type signature. (One possibility is to use RebindableSyntax essentially to disable number overloading, but that's a bit of a big hammer.)

The fact that the last example (with UnMaybed (Num a => a)) even compiles is very much a bug that will be file shortly.

Amendment

I found that you could actually implement this function without type families as follows.

{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances      #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE TypeFamilies #-}
module Main where

class UnMaybe x y where
    unMaybe :: x -> y

instance (a~a') => UnMaybe (Maybe a) a' where
    unMaybe (Just a) = a

instance (a~a') => UnMaybe a a' where
    unMaybe a = a

Notice that you still need the type family extension because of the equality constraint.

链接地址: http://www.djcxy.com/p/78248.html

上一篇: 隐式参数和类型族

下一篇: 重叠/不连续的封闭类型族