witness

values that witness types

https://github.com/AshleyYakeley/witness

Version on this page:	0.6.2
LTS Haskell 24.24:	0.7
Stackage Nightly 2025-12-16:	0.7
Latest on Hackage:	0.7

See all snapshots witness appears in

BSD-2-Clause licensed by Ashley Yakeley

Maintained by <[email protected]>

This version can be pinned in stack with:witness-0.6.2@sha256:4beb4195ecabeb5a26bf58c308d35f149a02dd5f86bd3b89c1cf8349f8b85f28,3613

Module documentation for 0.6.2

Data
- Data.PeanoNat
- Data.Type
  - Data.Type.Witness
    - Data.Type.Witness.Apply
    - Data.Type.Witness.General
      - Data.Type.Witness.General.AllConstraint
      - Data.Type.Witness.General.Finite
      - Data.Type.Witness.General.HetConstraint
      - Data.Type.Witness.General.ListElement
      - Data.Type.Witness.General.Order
      - Data.Type.Witness.General.Representative
      - Data.Type.Witness.General.TestHetEquality
      - Data.Type.Witness.General.WitnessConstraint
      - Data.Type.Witness.General.WitnessValue
    - Data.Type.Witness.Specific
      - Data.Type.Witness.Specific.All
      - Data.Type.Witness.Specific.ApplyStack
      - Data.Type.Witness.Specific.Concat
      - Data.Type.Witness.Specific.Either
      - Data.Type.Witness.Specific.Empty
      - Data.Type.Witness.Specific.FiniteAllFor
      - Data.Type.Witness.Specific.FixedList
      - Data.Type.Witness.Specific.List
        Data.Type.Witness.Specific.List.Element
        
        Data.Type.Witness.Specific.List.List
        
        Data.Type.Witness.Specific.List.Product
        
        Data.Type.Witness.Specific.List.Sum
      - Data.Type.Witness.Specific.Natural
      - Data.Type.Witness.Specific.OrderedWitnessMap
        Data.Type.Witness.Specific.OrderedWitnessMap.For
        
        Data.Type.Witness.Specific.OrderedWitnessMap.Of
      - Data.Type.Witness.Specific.Pair
      - Data.Type.Witness.Specific.PeanoNat
      - Data.Type.Witness.Specific.Single
      - Data.Type.Witness.Specific.Some
      - Data.Type.Witness.Specific.Symbol
      - Data.Type.Witness.Specific.WitnessMap
        Data.Type.Witness.Specific.WitnessMap.For
        
        Data.Type.Witness.Specific.WitnessMap.Of

Depends on 4 packages(full list with versions):

base, constraints, containers, countable

Used by 2 packages in nightly-2024-01-10(full list with versions):

monadology, open-witness

A witness is a value that witnesses some sort of constraint on some list of type variables. This library provides support for a wide variety of witness types. It also provides classes for representatives, which are values that represent types.

Changes

[0.6.2] - 2023-07-25

withAllConstraint, withSomeAllConstraint
listTypeToListM, listTypeForList, listTypeFind
fixedListLength, fixedListGenerate, Eq FixedList

[0.6.1] - 2022-09-12

new ListLength type family and associated functions
new Greater type family and associated functions
new FixedList type indexed by PeanoNat
new ListElement functions
new OrderedWitnessMapFor and OrderedWitnessMapOf types
new functions:
- someForToSome

[0.6] - 2022-05-08

reorganise modules
rename types and functions
additional functionality