Преобразовать список уровня типа '[a, b, c,] в функцию a- ›b-› c- ›

У меня есть семейство данных, проиндексированное списком на уровне типов, где типы в списке соответствуют параметрам экземпляра данных. Я хочу написать функцию, которая будет иметь разную арность и параметры в зависимости от экземпляра данных, чтобы я мог использовать ее как синоним для каждого экземпляра данных в семье.

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
             TypeFamilies, FlexibleInstances, PolyKinds #-}

module Issue where


type family (->>) (l :: [*]) (y :: *) :: * where
    '[]       ->> y = y
    (x ': xs) ->> y = x -> (xs ->> y)

class CVal (f :: [*]) where
    data Val f :: *
    construct :: f ->> Val f

instance CVal '[Int, Float, Bool] where
    data Val '[Int, Float, Bool] = Val2 Int Float Bool
    construct = Val2

Это нормально компилируется. Но когда я пытаюсь применить construct функцию:

v :: Val '[Int, Float, Bool]
v = construct 0 0 True

выдает ошибку:

Couldn't match expected type `a0
                              -> a1 -> Bool -> Val '[Int, Float, Bool]'
            with actual type `f0 ->> Val f0'
The type variables `f0', `a0', `a1' are ambiguous
The function `construct' is applied to three arguments,
but its type `f0 ->> Val f0' has none
In the expression: construct 0 0 True
In an equation for `v': v = construct 0 0 True

haskell type-level-computation type-families
person Alexey Vagarenko    schedule 01.07.2015    source источник

Ответы (1)


arrow_upward
7
arrow_downward

В вашем коде не удается выполнить проверку типов, поскольку семейства типов не являются (обязательно) инъективными. Если вы поможете GHC, указав выбор f в f ->> Val f, то он будет работать, как ожидалось:

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
             TypeFamilies, FlexibleInstances, PolyKinds #-}

module Issue where

import Data.Proxy

type family (->>) (l :: [*]) (y :: *) :: * where
    '[]       ->> y = y
    (x ': xs) ->> y = x -> (xs ->> y)

class CVal (f :: [*]) where
    data Val f :: *
    construct :: proxy f -> f ->> Val f

instance CVal '[Int, Float, Bool] where
    data Val '[Int, Float, Bool] = Val2 Int Float Bool deriving Show
    construct _ = Val2

v :: Val '[Int, Float, Bool]
v = construct (Proxy :: Proxy '[Int, Float, Bool]) 0 0 True

Ключевым моментом является передача этого Proxy :: Proxy '[Int, Float, Bool] аргумента в construct, тем самым фиксируя выбор f. Это потому, что ничто не мешает вам иметь такие типы f1 и f2, что f1 ->> Val f1 ~ f2 ->> Val f2.

Не волнуйтесь, этот недостаток языка рассматривается.

person Cactus    schedule 01.07.2015
comment
Ничто не мешает вам иметь такие типы f1 и f2, что f1 ->> Val f1 ~ f2 ->> Val f2. Фактически, есть: (->>) закрыто, а Val - это семейство данных (а не семейство типов), следовательно, инъективное. К сожалению, GHC просто не использует преимущества замкнутости семейств типов во время каких-либо рассуждений (пока?). - person Daniel Wagner; 01.07.2015