Il modulo GHC.TypeLits fornisce attualmente natVal
e symbolVal
, che ci consentono di ottenere un valore di runtime da un tipo di tipo Nat
o Symbol
. C'è un modo per ottenere un valore di runtime di tipo [String]
di un tipo di tipo '[Symbol]
? Non riesco a vedere un modo ovvio per farlo. Posso pensare a uno che utilizza una classe di caratteri con OverlappingInstances
, ma sembra che GHC dovrebbe già avere una funzione per questo.Converti Elenco livello di tipo in un valore
risposta
symbolVal
può essere mappato su elenchi di livello tipo. Per fare ciò abbiamo bisogno di ScopedTypeVariables
e PolyKinds
oltre a DataKinds
e TypeOperators
.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
import Data.Proxy
import GHC.TypeLits
avremo definito la classe dei tipi (di qualsiasi tipo), per il quale siamo in grado di "ottenere un valore di runtime di tipo [String]
".
class SymbolVals a where
symbolVals :: proxy a -> [String]
Possiamo ottenere un elenco di stringhe per qualsiasi elenco vuoto di tipi.
instance SymbolVals '[] where
symbolVals _ = []
Siamo in grado di ottenere una lista di stringhe per qualsiasi elenco dei tipi di cui possiamo ottenere una stringa per il primo tipo e un elenco di stringhe per la parte restante.
instance (KnownSymbol h, SymbolVals t) => SymbolVals (h ': t) where
symbolVals _ = symbolVal (Proxy :: Proxy h) : symbolVals (Proxy :: Proxy t)
Ah, molto bene. Ho dimenticato che questo non sarebbe uno scenario che richiedeva 'OverlappingInstances' perché i tipi' '[] 'e' (h': t) 'non si sovrappongono. Grazie. –
Suggerisco di utilizzare la libreria singletons
. Avete tutto il necessario ma utilizzando Sing
invece di Proxy
Tipo:
$ stack ghci --package singletons
Configuring GHCi with the following packages:
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XDataKinds
Prelude> import Data.Singletons.Prelude
Prelude Data.Singletons.Prelude> fromSing (sing :: Sing '["a","b"])
["a","b"]
Prelude Data.Singletons.Prelude> :t fromSing (sing :: Sing '["a","b"])
fromSing (sing :: Sing '["a","b"]) :: [String]
Sei interessato a qualcosa di simile a 'Forall (xs :: [Symbol]) -> HList XS -> [String]' o 'forall (xs :: [Symbol]) -> Proxy xs -> [String] '. Il primo è semplice, il secondo è leggermente meno semplice (avrete bisogno di un vincolo di classe di tipo su xs). – user2407038
Sto cercando il secondo. Anche se sarei curioso di vedere come viene fatto anche il primo (ma mi sembra che il tipo 'HList (xs :: '[Symbol])' sia più come una lista di liste). Inoltre, non ho mai visto il 'forall' usato in quel modo. Non dovrebbe esserci un periodo dopo la cosa che quantifica? –