Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,251
    • Issues 4,251
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 395
    • Merge Requests 395
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Wiki
    • Type nats
  • implementation

Last edited by diatchki Apr 09, 2012
Page history New page

implementation

The only "magic" thing about GHC.TypeLits are the instances of SingI. The rest is implemented like this:

newtype Sing n = Sing (SingRep n)

type family SingRep a
type instance SingRep (n :: Nat) = Integer
type instance SingRep (n :: Symbol) = String

fromSing :: Sing n -> SingRep n 
fromSing (Sing n) = n

So, now we just need instances like these:

instance SingI 0       where sing = Sing 0
instance SingI 1       where sing = Sing 1
instance SingI "hello" where sing = Sing "hello"
...

Because we cannot generate this infinite family of instances, we have some code in GHC which can solve SingI predicates on the fly.

The "proof" (aka "dictionary") for SingI n is just the number (or string) n. This is OK because:

  1. GHC uses a newtype to represent the dictionaries for classes that have just a single method and no super-classes. SingI is just such a class.
  2. Sing is already a newtype for Integer or String, depending on the kind of its parameter.

Therefore, the dictionaries for class SingI are just integers or strings, depending on the kind of the parameter.

Clone repository

GHC Home
GHC User's Guide

Joining In

Newcomers info
Mailing Lists & IRC
The GHC Team

Documentation

GHC Status Info
Working conventions
Building Guide
Debugging
Commentary

Wiki

Title Index
Recent Changes