How to use type-level literal numbers in singletons?

Question

I want to use singletons to represent ports at the type level, with type literals for the port numbers. Something like this:

data Port = Port Integer

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

bar :: Port
bar = fromSing foo

Short form of question is, how to implement this, or something resembling it?

I tried using singletons-2.0.1 with 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’
     In the expression: toSing b_a4Vk :: SomeSing (KProxy :: KProxy Nat)

So, sounds like it wants data Port = Port Integer, but that also fails to build too:

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.

I managed to get further than this, although not all the way, by not using the singletons library, but implementing a simplified version myself.

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

So far, so good, now this works:

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

But I'm stuck implementing fromSing for Port.

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

This fails with the same type error as shown for the first use of the singletons library above. And now, it's clear why: the SingKind instance for Nat produces an Integer, not a Nat. It seems it has to, because natVal produces an Integer.

So, I'm stuck!

The core problem is that the type Port is uninhabited, because the type Nat is uninhabited. singletons will generate type DemoteRep ('KProxy :: KProxy Port) = Port so any implementation of {to/from}Sing will necessarily be wrong. The simplest solution is to define data Port a = Port a and make singletons for that type, which allows you to have DemoteRep ('Port (n :: Nat)) ~ Port Integer. This will properly give you e.g. toSing (Port (10 :: Integer)) :: SomeSing ('KProxy :: KProxy (Port Nat)) — user2407038

Justin L. Justin L. · Accepted Answer · 2016-04-12T03:04:05

The main singletons idiom right now is to parameterize Port:

data Port nat = Port nat

(wrapped in the corresponding singletons quasiquoter, of course)

And, your normal data-level Port would be:

type Port' = Port Integer

and your type-level Port would be:

Port Nat

(which isn't yet allowed as a kind synonym, but should be allowed in GHC 8.0)

So, you have the type Port Integer inhabited by the values Port 1, Port 2, etc., and the kind Port Nat inhabited by the types Port 1, Port 2, etc.

The reason why this works out with the singletons library is because Integer is the singleton for Nat, so the singleton for Port Nat is Port Integer, automatically, for free. So everything works out like you'd expect when you use SingI, Sing, toSomeSing, etc. -- reflecting a Port Nat-kinded type will give you a Port Integer-type value, and reifying a Port Integer-type value will give you a Port Nat-kinded type.

How to use type-level literal numbers in singletons?

2 Answers