小编Joe*_*oey的帖子

Propellor代表它所部署的系统[Property],为了简化起见,我们可以这么说data Property = Property (Set Port) SatisfyProperty

因此,可能存在apacheInstalled使用端口80和443的torBridge属性,以及使用端口443 的属性.对于系统同时具有两个属性没有意义,因为它们使用相同的端口443.

我想知道类型检查器是否有可行的方法来阻止系统被分配？然后可以在构建时捕获端口冲突.我认为类型级别Ints将是第一步,但我对第二步没有任何线索.

我想使用单例来表示类型级别的端口,并使用端口号的类型文字.像这样的东西:

data Port = Port Integer

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

bar :: Port
bar = fromSing foo

简短的问题是,如何实现这个,或类似的东西？

我尝试使用单片机2.0.1和ghc-7.10.3

{-# 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’ …

使用单例库,这个简单的函数编译和工作.但是,ghci和ghc不同意它的类型签名,如果他们的任何一个建议被粘贴到代码中,它将无法编译.

GHC接受什么类型的签名？ghc-7.10.3,单身人士-2.0.1

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

import Data.Proxy (KProxy(..))
import Data.Singletons
import Data.Singletons.Prelude

-- ghc rejects this type signature, but if I leave it off, ghci :t shows exactly this.
matches :: (Eq (DemoteRep 'KProxy), SingKind 'KProxy) => DemoteRep 'KProxy -> Sing a -> Bool
matches m s = m == fromSing s

t :: Sing True
t = sing

demo :: Bool
demo = matches True t

上述类型签名的GHC错误:

Couldn't match type …