Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Struggling to get even the most basic usage of Data.Singletons.TypeLits.Nat to compile #76

Closed
CRogers opened this Issue May 25, 2014 · 5 comments

Comments

Projects
None yet
3 participants
@CRogers
Copy link

commented May 25, 2014

Hi,

I'm trying to use Nat as exported by Data.Singletons.TypeLits on GHC 7.8.2 but can't get even the most basic piece of code to compile:

{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, GADTs, DataKinds, TypeFamilies #-}

import Data.Singletons.TH
import Data.Singletons.TypeLits

singletons [d|
    data Foo = Bar Nat
 |]

Errors with:

Couldn't match type ‘Integer’ with ‘Nat’
Expected type: DemoteRep 'KProxy
  Actual type: Nat
In the first argument of ‘toSing’, namely ‘b_ayYo’
In the expression: toSing b_ayYo :: SomeSing (KProxy :: KProxy Nat)

If I use my own version of Nat instead (data Nat = Z | S Nat) it all works fine. Am I doing something wrong/misunderstanding something, or is the functionality not working as expected?

@jstolarek

This comment has been minimized.

Copy link
Collaborator

commented May 26, 2014

I can offer a partial explanation. The problem is that at the term level one usually uses Int or Integer, whereas at the type level the kind of numeric literals is Nat. However Nats don't exist at the term level, so term-level data definition that you want to singletonize cannot work. In the Prelude provided by singletons we work around this issue for the promotion case (but not for singletonization) by rewriting term-level functions that use Int to use Nat:

$(promoteOnly [d
  length :: [a] -> Nat
  length []     = 0
  length (_:xs) = 1 + length xs
 |])

Notice that length is promoted using promoteOnly, which discards the original term-level definition. This means that at the term level user has access to length from Prelude, which returns an Int, whereas at the type level the user has access to our promoted Length, which returns a Nat. This is still not perfect as there can be a mismatch in the semantics: while at the term level you can represent negative numbers, you can't do the same at the type level. I don't think this is fixable with the current treatment of promoted numeric literals in GHC.

See also #64.

That said, I am really puzzled about the error message. I wonder where does this Integer even come from. Richard?

@CRogers

This comment has been minimized.

Copy link
Author

commented May 26, 2014

Ah, thanks. So there's no way to use the TypeLits from GHC in singletons? That's unfortunate - I'm already getting inferred types like

Sing ('IntTy (Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ ('Succ 'Zero)))))))))))))))))

:p . Although, this can be mitigated with type synonyms somewhat but it would be nice to just see IntTy 32. Regarding the Integer, I would guess it comes from DemoteRep typefamily? I'm not sure though, as I'm still grokking/having my mind melted by the ideas behind this.

Keep up the good work with the library :)

@jstolarek

This comment has been minimized.

Copy link
Collaborator

commented May 26, 2014

So there's no way to use the TypeLits from GHC in singletons?

If you only want promotion there's the workaround that I've mentioned. If you want singletonization then I guess that at the moment the answer is "no". We're still missing some definitions - see #63. But I admit I'm not sure what happens once we have those definitions. Richard needs to speak here - he's the expert on singletonization.

Regarding the Integer, I would guess it comes from DemoteRep typefamily?

Oh, don't know how did I miss that.

@CRogers

This comment has been minimized.

Copy link
Author

commented May 26, 2014

I get the same kind of error when using Symbol too - I guess for the same reasons (no term level representation).

@goldfirere

This comment has been minimized.

Copy link
Owner

commented May 26, 2014

Yes, Jan is right. The short version is that built-in singletonization of datatypes that use the TypeLits Nat will not work. This is essentially because term-level Nat (which is an empty type) is different from type-level Nat (which is filled with numbers).

But, I think you can get away with writing your own singleton that will work:

data Foo = Bar Nat
data FooTerm = BarTerm Integer   -- Integer is the closest term-level equiv.

data instance Sing (x :: Foo) where
  SBar :: Sing n -> Sing (Bar n)

instance SingKind ('KProxy :: KProxy Foo) where
  type DemoteRep ('KProxy :: KProxy Foo) = FooTerm
  fromSing (SBar n) = BarTerm (fromSing n)
  toSing (BarTerm n) = case toSing n of
               SomeSing n' -> SomeSing (SBar n')

singletons normally takes advantage of the fact that a singleton is generally quite similar to the original, unpromoted type (for a specific definition of "quite similar"). When dealing with TypeLits, though, this correspondence doesn't hold. So, we have to define separate a datatype Foo to be promoted and singletonized and FooTerm to be the "base" datatype.

Alternatively, you could just omit the SingKind instance, if you don't need that functionality.

I imagine this would work very similarly with Symbol.

I will update the README to reflect this limitation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.