Convertire la lista di livello tipo '[a, b, c, ...] per funzionare a-> b-> c->

Question

Ho una famiglia di dati indicizzata per tipo di livello, dove i tipi in una lista corrispondono a parametri di un'istanza di dati. Voglio scrivere una funzione che avrà arit e parametri diversi a seconda di un'istanza di dati, quindi potrei usarla come sinonimo per ogni istanza di dati nella famiglia.

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

Questo compila bene. Ma quando cerco di applicare construct funzione:

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

produce errore:

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 

Answer 1

Il codice non riesce a TYPECHECK perché type families are not (necessarily) injective. Se aiutate fuori GHC specificando la scelta di f in f ->> Val f, allora funziona come previsto:

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

Il punto chiave sta passando che Proxy :: Proxy '[Int, Float, Bool] argomento construct, fissando in tal modo la scelta di f. Questo perché non c'è nulla che ti trattiene dall'avere tipi f1 e f2 tali che f1 ->> Val f1 ~ f2 ->> Val f2.

Non preoccuparti, this shortcoming of the language is being looked at.