{-# LANGUAGE RequiredTypeArguments, DataKinds, TypeFamilies, UndecidableInstances,

Question

{-# LANGUAGE RequiredTypeArguments, DataKinds, TypeFamilies, UndecidableInstances,

DerivingStrategies #-}

module Main where

import GHC.TypeLits
import Data.Type.Bool
import GHC.Types
import Data.Word

main = print (64 `is` Word6)

data Proxy a = MkProxy

is :: forall (n :: Nat) -> KnownNat n => forall a -> TypedFromIntegral n a => a
is n a = fromIntegralTyped @n @a MkProxy

class TypedFromIntegral n a where
fromIntegralTyped :: KnownNat n => Proxy n -> a

newtype Word6 = MkWord6 Word8
deriving newtype Show

instance CheckWord6Size n => TypedFromIntegral n Word6 where
fromIntegralTyped p = MkWord6 $ fromIntegral (natVal p)

type EmptyConstraints :: Constraint
type EmptyConstraints = () -- hack to make kind inference work for (% %)

type CheckWord6Size :: Nat -> Constraint
type family CheckWord6Size n where
CheckWord6Size n =
If (2 ^ 6 <=? n)
(TypeError (Text "Nat Is Out Of Bounds Word6"))
EmptyConstraints

#haskell #programming #russian

0

26.01.2024

1 ответов

12 просмотров

Danila Danko · Answer 1

Danila Danko

Стикер

0

3 месяца назад

169 похожих чатов

{-# LANGUAGE RequiredTypeArguments, DataKinds, TypeFamilies, UndecidableInstances,

1 ответов

Похожие вопросы