Come posso dire a GHC di soddisfare un vincolo <= a livello di tipo se so che è vero in fase di esecuzione?
Ho un tipo parametrizzato da un numero naturale n
:
data MyType (n :: Nat) = MyType
Le operazioni su questo tipo hanno senso solo quando n > 0
, quindi l'ho specificato come vincolo:
myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id
(Si noti che le versioni reali di queste funzioni fanno uso n
, trasformandola in un valore con natVal
.)
Voglio creare un tipo esistenziale ( SomeMyType
) che ci consenta di scegliere un n
in fase di esecuzione:
data SomeMyType where
SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType
Per produrre valori di SomeMyType
, sto scrivendo una someMyTypeVal
funzione che funziona come someNatVal
:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
| n > 0 = case someNatVal n of
Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
Nothing -> Nothing
| otherwise = Nothing
Questo funzionerebbe perfettamente senza il 1 <= n
vincolo, ma con il vincolo ottengo il seguente errore di tipo:
• Couldn't match type ‘1 <=? n’ with ‘'True’
arising from a use of ‘SomeMyType’
Come posso aggirare questa limitazione? Dato che l'ho verificato n > 0
in fase di runtime, non mi dispiacerebbe usare un'operazione come unsafeCoerce
qui per convincere GHC che 1 <= n
è vero, ma non posso usarla semplicementeunsafeCoerce
perché perderebbe il valore a livello di tipo di n
.
Qual è il modo migliore per affrontare questo problema?
Risposte
Dopo aver cercato un po 'di più, ho trovato la risposta di Justin L a una domanda simile . Ha racchiuso la sua soluzione nel typelits-witnessespacchetto che sono stato in grado di utilizzare per risolvere questo problema in modo abbastanza pulito:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
where check :: SomeNat -> Maybe SomeMyType
check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
LE Refl -> Just (SomeMyType (MyType @n))
NLE _ _ -> Nothing
a %<=? b
ci consente di confrontare due numeri naturali a livello di tipo e ci fornisce un testimone per sapere se a
è minore di b
( LE
) o meno ( NLE
). Questo ci dà il vincolo in più nel LE
caso di restituire a SomeMyType
, ma provare a farlo nel NLE
caso ci darebbe comunque l'errore "non può corrispondere '1 <=? N' con '' True" ".
Nota la firma del tipo esplicito per: check
senza di essa, il tipo di check
viene dedotto come check :: SomeNat -> Maybe a
e otterrei il seguente errore di tipo:
• Couldn't match type ‘a’ with ‘SomeMyType’
‘a’ is untouchable
inside the constraints: 'True ~ (1 <=? n)
Con la firma del tipo esplicito tutto funziona e il codice è anche (ragionevolmente) leggibile.
Come risposta più diretta, il vincolo 1 <= n
è solo un alias di tipo per 1 <=? n ~ 'True
. È possibile creare in modo non sicuro un tale vincolo di uguaglianza di tipo con:
{-# LANGUAGE DataKinds, TypeOperators #-}
import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce
unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl
che è più o meno quello che typelits-witnesses
sta facendo sotto il cofano.
Con quella definizione in atto, quanto segue dovrebbe controllare il tipo:
someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
| n > 0 = case someNatVal n of
Just (SomeNat (pxy :: p n)) ->
case unsafeDeclarePositive pxy of
Refl -> Just (SomeMyType (MyType @n))
Nothing -> Nothing
| otherwise = Nothing