sweirich / challenge Goto Github PK

challenge/debruijn$ cabal build
src/Imports.hs:30:1: error:
Could not find module ‘Data.Singletons.Prelude.Eq’
Perhaps you meant Data.Singletons.Decide (from singletons-3.0)
Use -v (or :set -v in ghci) to see a list of the files searched for.
|
30 | import Data.Singletons.Prelude.Eq
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Imports.hs:31:1: error:
Could not find module ‘Data.Singletons.Prelude.Enum’
Use -v (or :set -v in ghci) to see a list of the files searched for.
|
31 | import Data.Singletons.Prelude.Enum
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Imports.hs:32:1: error:
Could not find module ‘Data.Singletons.Prelude.Num’
Use -v (or :set -v in ghci) to see a list of the files searched for.
|
32 | import Data.Singletons.Prelude.Num
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Imports.hs:33:1: error:
Could not find module ‘Data.Singletons.Prelude’
Perhaps you meant
Data.Singletons.Decide (from singletons-3.0)
Data.Singletons.Bool (needs flag -package-key singleton-bool-0.1.5)
Use -v (or :set -v in ghci) to see a list of the files searched for.
|
33 | import Data.Singletons.Prelude
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/Imports.hs:34:1: error:
Could not find module ‘Data.Singletons.TH’
Perhaps you meant
Data.Singletons (from singletons-3.0)
Data.Singletons.Bool (needs flag -package-key singleton-bool-0.1.5)
Data.Singletons.Sigma (from singletons-3.0)
Use -v (or :set -v in ghci) to see a list of the files searched for.
|
34 | import Data.Singletons.TH
| ^^^^^^^^^^^^^^^^^^^^^^^^^

This isn't a bug report so much as a response to a challenge you posed during your Chalmers FP talk. And who am I to back down from a challenge? :)

If I understood you correctly, the reason that VarTy is defined like it is below:

Is due to a restriction in singletons. That is, VarTy uses a "simply typed" Idx (which is just a synonym for Nat) since it promoted/singles more easily using singletons' TH machinery. The drawback of this approach is that VarTy doesn't track the scope of type variables in Tys. This would be possible if a "richly typed" version of Idx were used instead:

However, this doesn't play nicely with singletons' TH machinery out of the box, making it inconvenient to use. (Did I summarize that accurately? If not, that makes the rest of this moot.)

The good news is that singletons-2.7 (which requires GHC 8.10 or later) has a configurable setting that makes automatically promoting/singling Idx possible. The challenge with handling GADTs is that the TH machinery will try to generate an instance of the SingKind class. Unfortunately, SingKind's current design isn't well suited to dealing with GADTs. Luckily, you can disable the generation of SingKind instances altogether by using Data.Singletons.TH.Options, like so:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Idx where

import Control.Monad.Trans.Class
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.TH.Options

$(withOptions defaultOptions{genSingKindInsts = False} $
  singletons $ lift [d|
    data Nat = Z | S Nat

    data Idx :: Nat -> Type where
        FZ :: Idx (S n)
        FS :: Idx n -> Idx (S n)
  |])

Not having a SingKind instance for Idx n may impact your library, however, since the toSing method of SingKind is used in a couple of places. If so, you can always roll your own version of toSing fairly easily:

toSIdx :: Idx n -> SomeSing (Idx n)
toSIdx FZ     = SomeSing SFZ
toSIdx (FS n) =
  case toSIdx n of
    SomeSing sn -> SomeSing (SFS sn)

I haven't attempted to use the "richly typed" version of Idx in VarTy, as I'm unclear what sort of repercussions that would have on the rest of the design. But this should hopefully demonstrate that it is at least possible!

What happened to says.lhs (or any other LHS files) file that seems necessary for building documentation?

In Makefile:

all:
	lhs2tex sysf.lhs > sysf.tex
	pdflatex sysf.tex