Haskell как построить объект, имеющий зависимые типы

Question

Я использовал семейство типов в данных 'D', чтобы ограничить тип первого элемента в нем. Теперь мне нужно создать объект любого типа «D B1» или «D B2» из некоторых общих функций (например, middle_func). Но приведенный ниже код не работает. Любые предложения, как это сделать? или поставить аналогичные ограничения другим способом.

data A1 = A1 
data A2 = A2 

data B1 = B1 
data B2 = B2 

data C a b where 
    C1 :: Int → C a b 
    C2 :: Char → C A1 b 
    C3 :: Bool → C A1 B1 

type family ResT b where 
    ResT B1 = C A1 B1 
    ResT B2 = C A2 B2 

data D b where 
    D1 :: ResT B1 → C A1 B1 → D B1 
    D2 :: ResT b → C A1 b → D b 

-- This does not compile 
intermediate_func :: Int → D b 
intermediate_func i = D2 (C1 i) (C1 i) 

-- This works 
-- intermediate_func :: Int -> D B2 
-- intermediate_func i = D2 (C1 i) (C1 i) 
-- So does this 
-- intermediate_func :: Int -> D B1 
-- intermediate_func i = D2 (C1 i) (C1 i) 

Answer 1

Вам нужно доказательство того, что b является либо B1 или B2, а не что-нибудь еще. Как написано, можно было бы назвать intermediate_func :: Int → D String.

Вы можете передать такие доказательства через синглтон:

data S b where 
    SB1 :: S B1 
    SB2 :: S B2 

intermediate_func :: S b → Int → D b 
intermediate_func SB1 i = D2 (C1 i) (C1 i) 
intermediate_func SB2 i = D2 (C1 i) (C1 i) 

Если вы хотите, чтобы скрыть одноплодной аргумент типа S b, проверить this recent question. Вы можете достичь этого с помощью классов типов. Например.

class CB b where getSB :: S b 
instance CB B1 where getSB = SB1 
instance CB B2 where getSB = SB2 

intermediate_func :: SB b → Int → D b 
intermediate_func SB1 i = D2 (C1 i) (C1 i) 
intermediate_func SB2 i = D2 (C1 i) (C1 i) 

intermediate_func_short :: CB b => Int → D b 
intermediate_func_short = intermediate_func getSB 

Answer 2

Решение с использованием классов типа:

{-# LANGUAGE GADTs #-}                        
{-# LANGUAGE TypeFamilies #-}                      
module Temp where                         

data A1                            
data A2                            
data B1                            
data B2                            

data C a b where                         
    C1 :: Int -> C a b                        
    C2 :: Char -> C A1 b                        
    C3 :: Bool -> C A1 B1                       

class Intermediate b where                       
    type ResT b                          
    intermediate_func :: Int -> D b                     

data D b where                          
    D1 :: ResT B1 -> C A1 B1 -> D B1                    
    D2 :: ResT b -> C A1 b -> D b                     

instance Intermediate B1 where                      
    type ResT B1 = C A1 B1                       
    intermediate_func i = D2 (C1 i) (C1 i)                   

instance Intermediate B2 where                      
    type ResT B2 = C A2 B2                       
    intermediate_func i = D2 (C1 i) (C1 i)