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,263
    • Issues 4,263
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 417
    • Merge Requests 417
  • 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
  • interact1

Last edited by diatchki Dec 19, 2010
Page history New page

interact1

(NOTE: The rules involving constants but no computation could be generalized to work for variables as well, as long as we know that the variables are in the acceptable ranges. Such information could be computed from the <= model, perhaps.)

Top-level interactions for TypeNat:

TypeNat m

Top-level interactions for <=

m <= n   <=> {m <= n}
0 <= a   <=> True
a <= 0   <=> a ~ 0

Top-level interactions for +.

(m + n ~ k) <=> {m + n == k}

(m + a ~ n) <=> a ~ {n - m}    -- n >= m
(0 + a ~ b) <=> a ~ b

(a + b ~ a) <=> (b ~ 0)
(a + b ~ b) <=> (a ~ 0)

(a + a ~ b) <=> (2 * a ~ b)
(a + b ~ 0) <=> (a ~ 0, b ~ 0) -- XXX: Drop this, follows from <= rules?

(a + m ~ b) <=> (m + a ~ b)    -- simple normalization cuts down on some rules

Top-level interactions for *.

(m * n ~ k) <=> {m * n == k}
(m * a ~ n) <=> a ~ { n / m }    -- m `divides` n, False otherwise

(0 * a ~ b) <=> b ~ 0
(1 * a ~ b) <=> a ~ b
(m * a ~ a) <=> a ~ 0            -- 2 <= m

(a * b ~ 1) <=> (a ~ 1, b ~ 1)
(a * a ~ b) <=> a ^ 2 ~ b

(a * m ~ b) <=> (m * a ~ b)      -- simple normalization cuts down on some rules

Top-level interactions for ^

(m ^ n ~ k) <=> {m ^ n == k}

(m ^ a ~ n) <=> a ~ {log m n}   -- log (base m) of n exists, False otherwise
(1 ^ a ~ b) <=> b ~ 1
(m ^ a ~ a) <=> False           -- m /= 1

(a ^ m ~ n) <=> a ~ {root m n}  -- m-th root of n exists, False otherwise
(a ^ 0 ~ b) <=> b ~ 1
(a ^ 1 ~ b) <=> a ~ b
(a ^ m ~ a) <=> (a <= 1)        -- 2 <= m
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