История изменений
Исправление Miguel, (текущая версия) :
Короче, всё как всегда: с данными проще работать, чем с классами:
{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures #-}
module Main where
import GHC.TypeLits
import Data.Proxy
data LessThen255 n where LessThen255 :: (n <= 255) => LessThen255 n
data Proof2 :: (Nat -> *) -> * where Proof2 :: c n -> Proxy n -> Proof2 c
one :: LessThen255 n -> Proxy n -> Proof2 LessThen255
one = Proof2
Исходная версия Miguel, :
Короче, всё как всегда: с данными проще работать, чем с классами:
{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures #-}
module Main where
import GHC.TypeLits
import Data.Proxy
data LessThen255 n where LessThen255 :: (n <= 255) => LessThen255 n
data Proof2 :: (Nat -> *) -> * where
Proof2 :: c n -> Proxy n -> Proof2 c
one :: LessThen255 n -> Proxy n -> Proof2 LessThen255
one = Proof2