Тип вывода для объявленного экземпляра

Question

Я придумал хорошее упражнение, но не могу заставить его работать.

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

{-# 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 

Это, возможно, может быть сделано по-разному, и решение является неполным, но сейчас мне нужно понять, почему он жалуется, что нет ни одного случая для RomanJoiner (One IVX) (One IVX) b0, в то время как я думаю Я объявил такого столяра.

Answer 1

Проблема заключается в том, что экземпляры не выбраны на основе только одного, который работает: одно расширение FunctionalDependencies помогает получить еще вывод типа. Включив это и сообщив | a b -> c, что тип a # b можно сделать из типов a и b. К сожалению, это не единственное, что вам нужно сделать, потому что вы получите ошибку Functional dependencies conflict between instance declarations. Используя некоторые классы, определенные в HList (они могут быть определены в другом месте), конфликтующие два экземпляра могут быть объединены в один, где возможны два (или 3, если вы подсчитаете ошибку) возможных результатов, исходя из того, являются ли некоторые типы равными ,

пара комментариев по поводу этого решения уродства:

1. вы не должны повторить то, что происходит на уровне типа на уровне значения снова (hCond против HCond), если вы были ленивее Показать экземпляры (например, instance Show I where show _ = "I").

2. с более современным расширением 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) 
   
   -}