CODEWITHSUNDEEP
haskellgadtsingleton-type
helq
helq

Reputation: 1561

Algebraic Data Types using Nat (singleton library)

I've been trying to declare an Algebraic Data Type to operate at the level of types using the singletons library. I can do it without much trouble if I don't use in the constructors Nat, Symbol, Integer or String. For example:

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}

import           Data.Singletons
import           Data.Singletons.TH

$(singletons [d|
  data Dim where
    NS :: Dim -- no size
    D  :: Bool -> Dim
   deriving (Eq, Show)
  |])

main :: IO ()
main = do
  let b = case toSing (D True) of
            (SomeSing d) -> show $ fromSing d
  putStrLn b

But it fails if I change Bool for either Nat or Integer.

How can I define an Algebraic Data Type to work with constructors that take Nat or Integer at the type level?

Upvotes: 2

Views: 98

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

From the README I gather that this is not possible directly because of the special status of Nat, but it also links to a possible workaround (see the last comment in the Github issue below): wrap Nat in some datatypes that singletons can handle.

https://github.com/goldfirere/singletons/issues/76

Upvotes: 1

Related Questions