I have an example that uses 32 type-level Nat numbers to create a UINTn instance, and a function getValidUINTn that cretaes such a UINTn from a runtime integer.
The only problem is that I have to use template-haskell or hand-write 32 cases of them. I cannot seem to use constraints’ unsafeAxiom to convince the runtime that it is a ValidUINTn.
#!/usr/bin/env -S cabal run -v1
{- cabal:
build-depends: base, template-haskell, constraints
default-language: GHC2024
ghc-options: -Wall
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TemplateHaskell #-}
-- base
import GHC.TypeLits (KnownNat (natSing), SNat, fromSNat, natVal, withKnownNat, withSomeSNat)
-- template-haskell
import qualified Language.Haskell.TH as TH
-- constraints
import Data.Constraint (Dict, (\\))
import Data.Constraint.Unsafe (unsafeAxiom)
class KnownNat n => ValidUINTn n
-- | This represents the type information of an unsigned integer with n-bytes.
data UINTn where
UINTn :: ValidUINTn n => SNat n -> UINTn
-- ^ Show the fashionable "U8", "U16", ... "U256".
instance Show UINTn where
show (UINTn sn) = "U" <> show (natVal sn * 8)
-- | This top-level splice generates all 32 of 'ValidUINTn' instances.
flip foldMap [1..32] $ \i -> [d| instance ValidUINTn $(TH.litT (TH.numTyLit i)) |]
-- | Maybe create a valid 'UINTn' from a runtime integer.
getValidUINTn :: Integer -> Maybe UINTn
getValidUINTn x =
withSomeSNat x $ \maybeSn -> maybeSn >>=
\sn -> let n = fromSNat sn
-- this minimizes the need of template haskell code
g :: forall n. ValidUINTn n => Maybe UINTn
g = Just (UINTn (natSing @n))
-- create all 32 cases using template-haskell:
-- case n of 1 -> g @1; 2 -> g @2; ...; _ -> _;
in $(TH.caseE
(TH.varE 'n)
( map
(\i -> TH.match
(TH.litP (TH.integerL i))
(TH.normalB (TH.varE 'g `TH.appTypeE` TH.litT (TH.numTyLit i)))
[])
[1..32]
++ [ TH.match TH.wildP (TH.normalB (TH.conE 'Nothing)) [] ]
)
)
-- NOTE: This version doesn't work, using unsafeAxiom to create bogus Dict
getValidUINTn' :: Integer -> Maybe UINTn
getValidUINTn' x =
withSomeSNat x $ \maybeSn -> maybeSn >>=
\sn -> let n = fromSNat sn
in if n >= 1 && n <= 32 then withKnownNat sn (go sn) else Nothing
where go :: forall n. KnownNat n => SNat n -> Maybe UINTn
go sn = Just (UINTn sn) \\ (unsafeAxiom :: Dict (ValidUINTn n))
main :: IO ()
main = do
print $ getValidUINTn 4
print $ getValidUINTn 32
print $ getValidUINTn 33
-- This outputs bogus number
print $ getValidUINTn' 8
{-
Local Variables:
fill-column: 100
haskell-process-type: cabal-repl
haskell-process-load-or-reload-prompt: t
End:
-}
Note that, if relaxed the constraint to:
data UINTn where
UINTn :: KnownNat n => SNat n -> UINTn
Things then work, but then I lose the type-level check that the “n” should be valid (1 <= n <= 32).
If you want to do it safely, then I recommend this convenience function, which seems pretty reasonable. If you really want you can put your use of unsafeValid in there, instead of the TH.
uintnofSNat :: SNat n -> Maybe UINTn
uintnofSNat sn =
$(TH.caseE
(TH.varE 'n)
( map
(\i -> TH.match
(TH.litP (TH.integerL i))
(TH.normalB (TH.varE 'g `TH.appTypeE` TH.litT (TH.numTyLit i)))
[])
[1..32]
++ [ TH.match TH.wildP (TH.normalB [| Nothing |]) [] ]
)
)
where
n = fromSNat sn
-- this minimizes the need of template haskell code
g :: forall n. ValidUINTn n => Maybe UINTn
g = Just (UINTn (natSing @n))
-- | Maybe create a valid 'UINTn' from a runtime integer.
getValidUINTn :: Integer -> Maybe UINTn
getValidUINTn x =
withSomeSNat x $ \maybeSn -> maybeSn >>= uintnofSNat
It doesn’t seem to be too different from what I had. But I extracted the said unsafeValidUINTnx, and tried it, it doesn’t seem to work neither:
unsafeValidUINTn :: forall n. KnownNat n => Dict (ValidUINTn n)
unsafeValidUINTn = unsafeAxiom \\ (Dict @(KnownNat n))
-- NOTE: This version doesn't work, using unsafeAxiom to create bogus Dict
getValidUINTn' :: Integer -> Maybe UINTn
getValidUINTn' x =
withSomeSNat x $ \maybeSn -> maybeSn >>=
\sn -> let n = fromSNat sn
in if n >= 1 && n <= 32
then withKnownNat sn (go sn)
else Nothing
where go :: forall n. KnownNat n => SNat n -> Maybe UINTn
go sn = Just (UINTn sn) \\ unsafeValidUINTn @n
output:
Just U32
Just U256
Nothing
Just U37723328
The last number is still bogus; in fairness, it probably should have segfaulted if it is wrong…
Also, note that there is an alternative that I hadn’t mentioned: I could define a constraint kind type using type families from GHC.TypeLits:
type ValidINTn n = (KnownNat n, 1 <= n, n <= 32)
But using this will make every typeclasses that use this constraint UndicidableInstances, which is yuk.
(edit, I made such an example:)
type ValidUINTn' n = (KnownNat n, 1 <= n, n <= 32)
data UINTn' where
UINTn' :: ValidUINTn' n => SNat n -> UINTn'
instance Show UINTn' where
show (UINTn' sn) = "U" <> show (natVal sn * 8)
getValidUINTn'' :: Integer -> Maybe UINTn'
getValidUINTn'' x =
withSomeSNat x $ \maybeSn -> maybeSn >>=
\sn -> let n = fromSNat sn
in if n >= 1 && n <= 32 then withKnownNat sn (g sn) else Nothing
where g :: forall n. KnownNat n => SNat n -> Maybe UINTn'
g sn = Just (UINTn' sn) \\ unsafeAxiom @(1 <= n, n <= 32)
-- This requries: UndecidableSuperClasses
-- class ValidUINTn' n => Yuk' n where
-- yuk' :: [Char]
-- This is fine, if you define it in all functions
class Yuk n where
yuk :: ValidUINTn' n => [Char]
Ah, yes. I just double checked unsafeAxiom implementation, and understood why.
This is actually the main take away and lesson from this thread for me.
Also, your sense of “yuk” is way off. unsafeAxiom and unsafeCoerce are both vastly more distasteful than UndecidableInstances. Even TH is worse.
You are correct to say that. My selective preference of what extensions are “safe” is quite irrational, especially for instance-selection related extensions…
Regardless, for completeness, another approach is to break off the superclass, allowing unsafeAxiom to produce dictionaries for a trivial ValidUINTn_.