SingI and DataKinds

Learn
#1

I’m not well versed into singletons, but I’m not too sure why can’t I use withSing (from the singleton package) taking advantage of knowledge from Data Kinds?

For example, given the following data types:

infixr 0 :->
data Types
  = Value Types0
  | Lazy Types
  | LazyS Types
  deriving (Typeable,Eq)

data Types0
  = Z
  | (:->) Types Types
  deriving (Typeable,Eq)

$(genSingletons [''Types0, ''Types])

The following code fails to compile:

withTypeableType' :: forall (z :: Types) r. (Typeable z => r) -> r
withTypeableType' f = withSing $ \case
  (z :: Sing z) -> withTypeableType z f
  where
  withTypeableType :: forall (z :: Types) r. Sing z -> (Typeable z => r) -> r
  withTypeableType = undefined

With the following error message:

No instance for ‘SingI z’ arising from a use of ‘withSing’

My reasoning on why this should work, is that we know that z :: Types , and we have generated the SingI instances using the genSingletons splice.

would anyone be so kind to shine a light on why this isn’t possible?

#2

You know the kind of z, but you don’t know z itself. A singleton represents a specific type, or in the case of data kinds, a specific constructor which has been promoted to a type. The SingI instances generated by genSingletons will be SingI t0 => SingI ('Value t0), SingI t => SingI ('Lazy t), etc. The compiler is complaining because it’s looking for SingI z but it doesn’t know which of the Types constructors z would unify with.

I don’t know what you hope to accomplish with withTypeableType'; its signature is something of a mystery to me. Are you confusing Typeable Types, an instance you’ve derived, with Typeable (z :: Types), a family of instances I don’t think you have?

1 Like
#3

Ohh, that makes sense! Thank you very much.

I’m currently trying to build my first type checker as follows:

-- I believe that I need an existential in order to be able to instantiate the TypeChecker class
data Expr' where
  MkExpr' :: (Ctx b) => TypedAST b -> Expr'

class TC a where
  tc ::  MonadReader Gamma m => a -> m Expr'

-- typecheck expressions
instance TC UntypedExpr where
  tc ::  MonadReader Gamma m => UntypedExpr -> m  Expr'
  tc = undefined

-- typecheck terms
instance TC UntypedTerm where
 tc ::  MonadReader Gamma m => UntypedTerm -> m  Expr'
 tc = undefined

My issue was that in an instance, I needed to inject those dictionaries:

instance TC UntypedTerm where
  tc (App f1 t2) = do
     MkExpr' @sf f1' <- tc f1
     MkExpr' @sx t2' <- tc t2

    withSing @sf $ \case
      SValue sf@(sa :%-> (sb :: Sing n)) -> withSing @sx $ \case
        se -> case (fromSing sa, fromSing se) of
          (Value x, Value y) | x == y -> pure
            -- we need for the returned value to have a Ctx constraint.
            -- sb :: Types, and I know that Ctx only contains constraints with kind `Types`
            -- so we can inject Ctx
            $ withCtx' @n --  I would like to just use type-applications instead of pattern matching sb.
            $ withCtx sf
            $ withCtx sa
            $ MkExpr' ... -- things that also might need a (Ctx sa/sf => ...)

That’s why I need the strange signature :slight_smile:

#4

Hmm… I may not have fully understood what you’re aiming for, but from what I can see I think you’re trying to pass around too much run-time information in the type system.

You have this line:

MkExpr' @sf f1' <- tc f1`

which looks like it’s checking the untyped term f1 and giving you back a typed term f1' and binding the type sf (though sf, as a type, has no run-time representation). Then you’re attempting to match on the singleton corresponding to sf, but since sf isn’t known statically, there’s no way to produce the correct value for a run-time match to recognize.

If I have that right, I think your Expr' type ought to have fields for both the typed term and the type-in-your-language, and then you can match on the type-in-your-language instead of trying to construct a singleton from an unknown type-in-Haskell.

1 Like
#5

That’s good to know! and you also got that right!

But most importantly, thank you for letting me know that Expr' should have a field for the type-in-my-language. I thought I would be ok having Ctx b = (Typeable b, SingI b, ....), but the code got messy way too quick (as you can notice!).

It is truly invaluable to have this kind of feedback, most of the times I have to work in the dark without knowing if I’m taking the wrong approach, or it’s just that I’m lacking some key element that will make everything ok. So, thank you again!

#6

By the way, you should absolutely not need Typeable. I suspect any place you use Typeable is a place where something has gone wrong in your understanding. One way of seeing SingI, in fact, is that it’s a "well-typed version of Typeable". That is, rather than being able to inspect what type your type is from the “whole Haskell world of types” (Typeable) you can ask what type it is from the “appropriate sized subset” (SingI).

However, I don’t actually see you using Typeable, so I’m not sure if you just haven’t shared the parts of the code that use it or you’re not using it at all.

2 Likes
#7

that makes sense, originally, I just had a well typed GADT which represented the AST, and I needed a way to lookup variables, so I made something like Map String (SomeTypeRep,E env m Any) and then relied on Typeable to check the type.

It was only after I began writing a Parser + Typechecker that I came up with singletons (and rewrote the types of my language as a sum-type, instead of data Value a; data Lazy a; ...). So yes, that’s something I’ll have to clean up c:

1 Like
#8

Actually, your “typed expression of unknown type” was correct, I think, except that you shouldn’t use Ctx, you should use SingI. The point of SingI is to replace a whole bunch of other instances. They should all be derived from SingI itself!

Anyway, here’s how I’d do it. It’s not actually a practical example because it only contains unit and applications, but hopefully it serves as a sufficient example. Feel free to ask any questions!

{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TemplateHaskell #-}

import Data.Singletons.TH

infixr 0 :->

data Types
  = Z
  | (:->) Types Types
  deriving (Eq)

$(genSingletons [''Types])

-- This is, in principle, derivable. I don't know if there's
-- any library providing TH to derive it though.
eqKind :: STypes a -> STypes b -> Maybe (a :~: b)
eqKind = \case
  SZ -> \case
    SZ -> Just Refl
    _ -> Nothing
  a1 :%-> b1 -> \case
    a2 :%-> b2 -> do
      Refl <- eqKind a1 a2
      Refl <- eqKind b1 b2
      Just Refl
    _ -> Nothing

data UntypedExpr =
  UntypedZ
  | UntypedApp UntypedExpr UntypedExpr

data TypedExpr t where
  TypedZ :: TypedExpr Z
  TypedApp :: TypedExpr (a :-> b) -> TypedExpr a -> TypedExpr b

data Some f where
  MkSome :: SingI a => f a -> Some f

infer :: UntypedExpr -> Either String (Some TypedExpr)
infer = \case
  UntypedZ -> pure (MkSome TypedZ)
  UntypedApp f x -> do
    MkSome @sf f' <- infer f
    MkSome @sx x' <- infer x

    case sing @sf of
      SZ -> Left "f was not arrow type"
      a :%-> b -> case eqKind a (sing @sx) of
        Nothing -> Left "Type of x did not match argument type of f"
        Just Refl -> withSingI b (pure (MkSome (TypedApp f' x')))
1 Like
#9

Oh, I didn’t realize Ctx was holding a SingI. In that case, the SingI instance would be held in the MkExpr' constructor and that can serve the purpose of the field I was proposing, as long as you’re diligent about propagating that constraint everywhere it needs to go. Tom’s post should set you right.

If you haven’t found it yet, the Stitch paper may also be a good reference for you, as it implements a simple type-safe type checker using singletons.

2 Likes
#10

Depending on your use-case, you might not need singletons and you could use TypeRep from Type.Reflection. That’s what I’m doing in hell. I cite my sources in these slides, which includes a typed type checker by Stephanie Weirich, a total evaluator which has total variable lookups by Oleg, and type-class resolution I got from Eitan Chatav. I also recently have a branch in which I’ve successfully got well typed anonymous records working. You can go really far with just Type.Reflection!

A blog post comparing the relative ergonomics of TypeRep vs singletons would be a very niche but interesting thing to read. I personally wanted to emphasize a “thin” meta-circular Haskell, so I wanted a type and evaluator that doesn’t deviate from Haskell. I can imagine singletons coming in handy when I want the opposite.

2 Likes
#11

TypeRep is effectively the Sing for Type, and Typeable is its SingI. That is, these would be valid definitions:

type instance Sing @Type = TypeRep

instance Typeable t => SingI (t :: Type) where
    sing = typeRep

so Type.Reflection is a special case of singletons. If you use Type as your index type then you work with the whole universe of Haskell types (and because it’s an open universe one implication is that you can’t exhaustively pattern match). So I think the choice between the two comes down to whether you’re trying to make an interpreter for Haskell or for some smaller language.

4 Likes
#12

(‘Smaller’ here presumably refers to the surjectivity of the encoding, not the cardinality of the encoded set! It should be possible to use singletons to check a language with a ‘larger’ type system than Haskell too.)

2 Likes
#13

I meant “smaller” is the sense that Types and Types0 from the initial post are “smaller” than Data.Kind.Type. But yes, I guess you’re right, I probably should have said “some different language”.

2 Likes
#14

Thanks to everybody! Took some time, but I finally got everything refactored.

tomjaguarpaw → your eqKind was really useful in getting rid of (a lot) of nesting. I also made use of the Some and rid out of Typeable.

rhendric Thanks for the paper! As you can see, I was home-mading a typechecker without any theory to back it up, just my intuition. I’ll begin reading it to see what ideas can I borrow as soon as I finish my current goal (rewriting my untyped ADT/typed GADT into a single GADT a la trees that grow) :slight_smile:.

chrisdone Thank you for the slides! I didn’t know that Dict was a constructor for the implicit dictionaries! This was the one thing that stopped me from finishing my V1 using only Typeable/Reflection.

Again, thank you all for the amazing responses!

3 Likes