haskell - Type Inference for declared instance

Question

I came up with a nice exercise, but can't make it work.

The idea is to try and express Roman numerals in such a way that the type checker will tell me whether the numeral is valid.

    {-# LANGUAGE RankNTypes
               , MultiParamTypeClasses #-}

    data One a b c = One a deriving (Show, Eq)
    data Two a b c = Two (One a b c) (One a b c) deriving (Show, Eq)
    data Three a b c = Three (One a b c) (Two a b c) deriving (Show, Eq)
    data Four a b c = Four (One a b c) (Five a b c) deriving (Show, Eq)
    data Five a b c = Five b deriving (Show, Eq)
    data Six a b c = Six (Five a b c) (One a b c) deriving (Show, Eq)
    data Seven a b c = Seven (Five a b c) (Two a b c) deriving (Show, Eq)
    data Eight a b c = Eight (Five a b c) (Three a b c) deriving (Show, Eq)
    data Nine a b c d e = Nine (One a b c) (One c d e) deriving (Show, Eq)

    data Z = Z deriving (Show, Eq) -- dummy for the last level
    data I = I deriving (Show, Eq)
    data V = V deriving (Show, Eq)
    data X = X deriving (Show, Eq)
    data L = L deriving (Show, Eq)
    data C = C deriving (Show, Eq)
    data D = D deriving (Show, Eq)
    data M = M deriving (Show, Eq)

    i :: One I V X
    i = One I

    v :: Five I V X
    v = Five V

    x :: One X L C
    x = One X

    l :: Five X L C
    l = Five L

    c :: One C D M
    c = One C

    d :: Five C D M
    d = Five D

    m :: One M Z Z
    m = One M

    infixr 4 #

    class RomanJoiner a b c where
      (#) :: a -> b -> c

    instance RomanJoiner (One a b c) (One a b c) (Two a b c) where
      (#) = Two

    instance RomanJoiner (One a b c) (Two a b c) (Three a b c) where
      (#) = Three

    instance RomanJoiner (One a b c) (Five a b c) (Four a b c) where
      (#) = Four

    instance RomanJoiner (Five a b c) (One a b c) (Six a b c) where
      (#) = Six

    instance RomanJoiner (Five a b c) (Two a b c) (Seven a b c) where
      (#) = Seven

    instance RomanJoiner (Five a b c) (Three a b c) (Eight a b c) where
      (#) = Eight

    instance RomanJoiner (One a b c) (One c d e) (Nine a b c d e) where
      (#) = Nine

    main = print $ v # i # i

This possibly can be done differently, and the solution is incomplete, but right now I need to understand why it complains that there is no instance for RomanJoiner (One I V X) (One I V X) b0, whereas I think I declared such a joiner.

score 4 · Accepted Answer

问题是实例不是基于唯一有效的实例来选择的：一个扩展FunctionalDependencies有助于获得更多的类型推断。启用它，并说可以从 and 的类型推断出的| a b -> c类型。不幸的是，这不是您唯一需要做的事情，因为您会收到错误消息。使用在 HList 中定义的一些类（这些可以在其他任何地方定义），冲突的两个实例可以组合成一个实例，其中两个（或 3，如果您计算错误）可能的结果是根据某些类型是否相等来选择的.a # babFunctional dependencies conflict between instance declarations

关于这个解决方案丑陋的一些评论：

如果您有更惰性的 Show 实例（例如），则不必再次在值级别（hCondvs ）复制类型级别发生的事情。HCondinstance Show I where show _ = "I"

通过更现代的扩展，可以消除TypeFamilies许多中间类型变量。ba, bb, bc, babc ...

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FunctionalDependencies, ScopedTypeVariables, UndecidableInstances, FlexibleContexts, FlexibleInstances #-}
import Data.HList hiding ((#))
import Data.HList.TypeEqGeneric1
import Data.HList.TypeCastGeneric1
import Unsafe.Coerce

data One a b c = One a deriving (Show, Eq)
data Two a b c = Two (One a b c) (One a b c) deriving (Show, Eq)
data Three a b c = Three (One a b c) (Two a b c) deriving (Show, Eq)
data Four a b c = Four (One a b c) (Five a b c) deriving (Show, Eq)
data Five a b c = Five b deriving (Show, Eq)
data Six a b c = Six (Five a b c) (One a b c) deriving (Show, Eq)
data Seven a b c = Seven (Five a b c) (Two a b c) deriving (Show, Eq)
data Eight a b c = Eight (Five a b c) (Three a b c) deriving (Show, Eq)
data Nine a b c d e = Nine (One a b c) (One c d e) deriving (Show, Eq)

data Z = Z deriving (Show, Eq) -- dummy for the last level
data I = I deriving (Show, Eq)
data V = V deriving (Show, Eq)
data X = X deriving (Show, Eq)
data L = L deriving (Show, Eq)
data C = C deriving (Show, Eq)
data D = D deriving (Show, Eq)
data M = M deriving (Show, Eq)

i :: One I V X
i = One I

v :: Five I V X
v = Five V

x :: One X L C
x = One X

l :: Five X L C
l = Five L

c :: One C D M
c = One C

d :: Five C D M
d = Five D

m :: One M Z Z
m = One M

infixr 4 #

class RomanJoiner a b c | a b -> c where
    (#) :: a -> b -> c


instance RomanJoiner (One a b c) (Two a b c) (Three a b c) where
    (#) = Three

instance RomanJoiner (One a b c) (Five a b c) (Four a b c) where
    (#) = Four

instance RomanJoiner (Five a b c) (One a b c) (Six a b c) where
    (#) = Six

instance RomanJoiner (Five a b c) (Two a b c) (Seven a b c) where
    (#) = Seven

instance RomanJoiner (Five a b c) (Three a b c) (Eight a b c) where
    (#) = Eight

data Error = Error
instance forall a b c a' b' c' ba bb bc bab babc z bn nine.
   (TypeEq a a' ba,
    TypeEq b b' bb,
    TypeEq c c' bc,
    HAnd ba bb bab,
    HAnd bab bc babc,

    TypeEq c a' bn,
    HCond bn (Nine a b c b' c') Error nine,

    HCond babc (Two a b c) nine  z) =>
        RomanJoiner (One a b c) (One a' b' c') z where
    (#) x y = hCond (undefined :: babc)
                (Two (uc x :: One a b c) (uc y :: One a b c)) $
              hCond (undefined :: bn)
                (Nine (uc x :: One a b c) (uc y :: One c b' c'))
                Error
        where uc = unsafeCoerce

main = print $ v # i # i
{-
Prints with ghc 762, HList-0.2.3

*Main> main
Seven (Five V) (Two (One I) (One I)

-}

haskell - Type Inference for declared instance

1 回答 1

Related

Reference