सिंगलेट्स में टाइप-स्तरीय शाब्दिक संख्याओं का उपयोग कैसे करें?

Question

मैं पोर्ट नंबरों के लिए टाइप अक्षर के साथ प्रकार के स्तर पर बंदरगाहों का प्रतिनिधित्व करने के लिए सिंगलेट का उपयोग करना चाहता हूं। कुछ ऐसा:

data Port = Port Integer 

foo :: Sing ('Port 80) 
foo = sing 

bar :: Port 
bar = fromSing foo 

प्रश्न का संक्षिप्त रूप यह है कि इसे कैसे कार्यान्वित किया जाए, या ऐसा कुछ जैसा हो?

मैं GHC-7.10.3 साथ एकमात्र-2.0.1 उपयोग करने की कोशिश

{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, GADTs, KindSignatures, DataKinds, PolyKinds, TypeOperators, FlexibleContexts, RankNTypes, UndecidableInstances, FlexibleInstances, InstanceSigs, DefaultSignatures, DataKinds, PolyKinds #-} 

import Data.Singletons 
import Data.Singletons.TH 
import Data.Singletons.Prelude 
import GHC.TypeLits 

$(singletons [d| 
    data Port = Port Nat 
    |]) 

foo.hs:8:3: 
    Couldn't match type ‘Integer’ with ‘Nat’ 
    Expected type: DemoteRep 'KProxy 
     Actual type: Nat 
    In the first argument of ‘toSing’, namely ‘b_a4Vk’ 
    In the expression: toSing b_a4Vk :: SomeSing (KProxy :: KProxy Nat) 

तो, लगता है जैसे कि यह डेटा पोर्ट = पोर्ट पूर्णांक चाहता है, लेकिन वह भी बहुत निर्माण करने के लिए विफल रहता है:

foo.hs:8:3: 
    ‘Port’ of kind ‘*’ is not promotable 
    In the kind ‘Port -> *’ 
    In the type ‘(Sing :: Port -> *)’ 
    In the type declaration for ‘SPort’ 
Failed, modules loaded: none. 

मैं इस से आगे निकलने में कामयाब रहा, हालांकि सभी तरह से, सिंगलटन लाइब्रेरी का उपयोग न करके, लेकिन एक सरलीकृत संस्करण को लागू करना।

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies, GADTs, FlexibleInstances, UndecidableInstances, ScopedTypeVariables, FlexibleContexts #-} 

import GHC.TypeLits 
import Data.Proxy (KProxy(..), Proxy(..)) 

data Port = Port Nat 

data family Sing (x :: k) 

class SingI t where 
    sing :: Sing t 

class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where 
    type DemoteRep kparam :: * 
    fromSing :: Sing (a :: k) -> DemoteRep kparam 

type SNat (x :: Nat) = Sing x 
data instance Sing (n :: Nat) = KnownNat n => SNat 
instance KnownNat n => SingI n where sing = SNat 
instance SingKind ('KProxy :: KProxy Nat) where 
    type DemoteRep ('KProxy :: KProxy Nat) = Integer 
    fromSing (SNat :: Sing n) = natVal (Proxy :: Proxy n) 

data instance Sing (x :: Port) where 
     SPort :: Sing n -> Sing ('Port n) 
instance KnownNat n => SingI ('Port (n :: Nat)) where sing = SPort sing 

अब तक तो अच्छा, अब यह काम करता है:

foo :: Sing ('Port 80) 
foo = sing 

लेकिन मैं पोर्ट के लिए fromSing को लागू करने अटक कर रहा हूँ।

instance SingKind ('KProxy :: KProxy Port) where 
     type DemoteRep ('KProxy :: KProxy Port) = Port 
     fromSing (SPort n) = Port (fromSing n) 

यह उपरोक्त सिंगलटन लाइब्रेरी के पहले उपयोग के लिए दिखाए गए समान प्रकार की त्रुटि के साथ विफल रहता है। और अब, यह स्पष्ट है कि क्यों: नेट के लिए सिंगकिंड इंस्टेंस एक इंटीजर पैदा करता है, नाट नहीं। ऐसा लगता है कि ऐसा करना है, क्योंकि नेटवेल एक इंटीजर पैदा करता है।

तो, मैं अटक गया हूँ!

Answer 1

कुछ सिंगलटन के बिना, कुछ आसान होगा, आपके लिए काम करेगा?

{-# language DataKinds, ScopedTypeVariables #-} 

import Data.Proxy 
import GHC.TypeLits 

data Port = Port{ portNumber :: Integer } 
data PortT = PortT Nat 

webPort :: Proxy ('PortT 80) 
webPort = Proxy 

reify :: forall n. (KnownNat n) => Proxy ('PortT n) -> Port 
reify _ = Port (natVal (Proxy :: Proxy n)) 

यह आप

*Main> portNumber $ reify webPort 
80 

Answer 2

मुख्य एकमात्र मुहावरा देता है अभी parameterize करने के लिए है Port:

data Port nat = Port nat 

(quasiquoter, निश्चित रूप से इसी एकमात्र में लिपटे)

और, न ही आपका मल डेटा स्तरीय Port होगा:

type Port' = Port Integer 

और अपने प्रकार स्तरीय Port होगा:

Port Nat 

(जो अभी तक एक तरह का पर्याय के रूप में अनुमति नहीं है, लेकिन GHC 8.0 में अनुमति दी जानी चाहिए)

तो, आप प्रकारPort Integer मूल्यों Port 1, Port 2, आदि का निवास है, और तरहPort NatPort 1, Port 2, आदि के प्रकार से घिरा हुआ है।

कारण है कि इस एकमात्र क्योंकि IntegerNat के लिए सिंगलटन है, इसलिए Port Nat के लिए सिंगलटन Port Integer है, स्वचालित रूप से मुक्त करने के लिए पुस्तकालय है के साथ बाहर काम करता है। तो सब कुछ आप की तरह बाहर काम करता है उम्मीद थी जब तुम SingI, Sing, toSomeSing का उपयोग, आदि - एक Port Nat -kinded प्रकार को दर्शाती है कि आप एक Port Integer प्रकार मूल्य दे देंगे, और एक Port Integer प्रकार मूल्य reifying आप दे देंगे एक Port Nat - दयालु प्रकार।