wip Add fine-types-core package with Agda proofs

.gitignore

@@ -15,6 +15,10 @@
 *.hp
 *.eventlog
 
+### agda2hs ###
+_build
+*.agdai
+
 ### Cabal ###
 dist
 dist-*

lib/fine-types-core/CHANGELOG.md

@@ -0,0 +1,5 @@
+# Revision history for fine-types-core
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

lib/fine-types-core/README.md

@@ -0,0 +1,15 @@
+[FineTypes][] is an interface description language (IDL) focussing on types.
+
+  [finetypes]: https://github.com/cardano-foundation/fine-types
+
+The `fine-types-core` package defines the core data types and functions — and it includes machine-checked proofs!
+
+The proofs are written in Agda and the code is exported to Haskell using [agda2hs][].
+
+The repository layout includes:
+
+* `./src/agda` — Agda source code with proofs.
+* `./src/haskell` — Haskell source code that was **autogenerated** from the Agda code. These files are still checked into the repository.
+* `./generate-haskell.sh` — Script which uses [agda2hs][] to generate the Haskell source code. Run this script whenever you change the Agda source.
+
+  [agda2hs]: https://github.com/agda/agda2hs

lib/fine-types-core/fine-types-core.agda-lib

@@ -0,0 +1,3 @@
+name: fine-types-core
+include: ./src/agda
+depend: agda2hs, standard-library

lib/fine-types-core/fine-types-core.cabal

@@ -0,0 +1,63 @@
+cabal-version:      3.0
+name:               fine-types-core
+version:            0.1.0.0
+synopsis:           A interface description language (IDL) focusing on types
+description:        Core definitions and proofs for fine-types.
+homepage:           https://github.com/cardano-foundation/fine-types
+license:            Apache-2.0
+license-file:       LICENSE
+author:             HAL, Cardano Foundation
+maintainer:         hal@cardanofoundation.org
+copyright:          2023 Cardano Foundation
+category:           Language
+
+extra-doc-files:
+  CHANGELOG.md
+extra-source-files:
+  generate-haskell.sh
+  fine-types-core.agda-lib
+  src/agda/**/*.agda
+
+common language
+  default-language:
+    Haskell2010
+  default-extensions:
+    NoImplicitPrelude
+  other-extensions:
+    NamedFieldPuns
+    OverloadedStrings
+
+common opts-lib
+  ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
+
+  if flag(release)
+    ghc-options: -O2 -Werror
+
+common opts-exe
+  ghc-options: -threaded -rtsopts
+  ghc-options: -Wall -Wcompat -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates
+
+  if flag(release)
+    ghc-options: -O2 -Werror
+
+flag release
+  description: Enable optimization and `-Werror`
+  default:     False
+  manual:      True
+
+library
+  import:      language, opts-lib
+  hs-source-dirs:
+    src/haskell
+  build-depends:
+    , base >=4.14.3.0
+    , containers
+    , deepseq >= 1.4.4
+    , QuickCheck
+  exposed-modules:
+    Data.Embedding
+    Language.FineTypes
+    Language.FineTypes.Embedding
+    Language.FineTypes.Typ
+    Language.FineTypes.Value.Def
+    Language.FineTypes.Value.Typcheck

lib/fine-types-core/generate-haskell.sh

@@ -0,0 +1,2 @@
+#!/bin/sh
+agda2hs ./src/agda/Language/FineTypes.agda -o ./src/haskell/

lib/fine-types-core/src/agda/Data/Embedding.agda

@@ -0,0 +1,21 @@
+module Data.Embedding where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude
+
+{-----------------------------------------------------------------------------
+    Embedding
+------------------------------------------------------------------------------}
+record Embedding (a b : Set) : Set where
+  field
+    to   : a → b
+    from : b → a
+    @0 from∘to : ∀ (x : a) → from (to x) ≡ x
+
+open Embedding public
+
+{-# COMPILE AGDA2HS Embedding #-}

lib/fine-types-core/src/agda/Language/FineTypes.agda

@@ -0,0 +1,12 @@
+module Language.FineTypes where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+import Data.Embedding
+import Language.FineTypes.Typ
+import Language.FineTypes.Value.Def
+import Language.FineTypes.Embedding
+-- import Language.FineTypes.Value.Typcheck

lib/fine-types-core/src/agda/Language/FineTypes/Embedding.agda

@@ -0,0 +1,77 @@
+module Language.FineTypes.Embedding where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude hiding (_×_; _+_; Pair)
+open import Relation.Nullary using (¬_)
+
+open import Data.Embedding
+open import Language.FineTypes.Value.Def
+open import Language.FineTypes.Typ
+  using (Typ; _+_; _×_)
+
+import Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Embedding with Typ information
+------------------------------------------------------------------------------}
+record EmbeddingTyp (@0 A B : Typ) : Set where
+  field
+    embed    : Embedding (Value A) (Value B)
+    typcheck : Typ → Maybe Typ
+    @0 accepts : typcheck A ≡ Just B
+    @0 rejects : ∀ (C : Typ) → typcheck C ≡ Nothing → ¬(C ≡ A)
+
+open EmbeddingTyp public
+
+{-# COMPILE AGDA2HS EmbeddingTyp #-}
+
+{-----------------------------------------------------------------------------
+    Specific Embeddings
+------------------------------------------------------------------------------}
+distributeVal
+  : ∀ {@0 A B C : Typ}
+  → Embedding
+      (Value ((A + B) × C))
+      (Value ((A × C) + (B × C)))
+distributeVal =
+  record
+    { to = λ
+      { (Product2 (Sum2L a) c) → Sum2L (Product2 a c)
+      ; (Product2 (Sum2R b) c) → Sum2R (Product2 b c)
+      }
+    ; from = λ
+      { (Sum2L (Product2 a c)) → (Product2 (Sum2L a) c)
+      ; (Sum2R (Product2 b c)) → (Product2 (Sum2R b) c)
+      }
+    ; from∘to = λ
+      { (Product2 (Sum2L a) c) → refl
+      ; (Product2 (Sum2R b) c) → refl
+      }
+    }
+
+{-# COMPILE AGDA2HS distributeVal #-}
+
+distribute
+  : ∀ {@0 A B C : Typ}
+  → EmbeddingTyp
+      ((A + B) × C)
+      ((A × C) + (B × C))
+distribute =
+  record
+    { embed = distributeVal
+    ; typcheck = λ
+      { (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 a b) c)
+          → Just (Typ.Two Typ.Sum2 (Typ.Two Typ.Product2 a c) (Typ.Two Typ.Product2 b c))
+      ; _ → Nothing
+      }
+    ; accepts = refl
+    ; rejects = λ
+      { (Typ.Two Typ.Product2 (Typ.Two Typ.Sum2 _ _) _) → λ ()
+      }
+    }
+
+{-# COMPILE AGDA2HS distribute #-}

lib/fine-types-core/src/agda/Language/FineTypes/Typ.agda

@@ -0,0 +1,149 @@
+module Language.FineTypes.Typ where
+
+{-# FOREIGN AGDA2HS
+-- !!! This Haskell module has been autogenerated by agda2hs.
+-- !!! Do NOT change; change the original .agda file instead.
+#-}
+
+open import Haskell.Prelude
+  using (String; List; True; False)
+  renaming (_×_ to Pair)
+open import Haskell.Law.Eq
+open import Haskell.Prim.Eq
+
+import Haskell.Prelude as Hs
+
+ConstructorName = String
+FieldName = String
+TypName = String
+VarName = String
+
+{-# COMPILE AGDA2HS ConstructorName #-}
+{-# COMPILE AGDA2HS FieldName #-}
+{-# COMPILE AGDA2HS TypName #-}
+{-# COMPILE AGDA2HS VarName #-}
+
+{-----------------------------------------------------------------------------
+    Haskell - Typ
+------------------------------------------------------------------------------}
+data TypConst : Set where
+  Bool     : TypConst
+  Bytes    : TypConst
+  Integer  : TypConst
+  Natural  : TypConst
+  Text     : TypConst
+  Rational : TypConst
+  Unit     : TypConst
+
+data OpOne : Set where
+  Option   : OpOne
+  Sequence : OpOne
+  PowerSet : OpOne
+
+data OpTwo : Set where
+  Sum2     : OpTwo
+  Product2 : OpTwo
+  PartialFunction : OpTwo
+  FiniteSupport   : OpTwo
+
+data Constraint1 : Set where
+  Braces : List Constraint1 → Constraint1
+  Token  : String → Constraint1
+
+Constraint = List Constraint1
+
+data Typ : Set where
+  Var  : TypName → Typ
+  Zero : TypConst → Typ
+  One  : OpOne → Typ → Typ
+  Two  : OpTwo → Typ → Typ → Typ
+  ProductN : List (Pair FieldName Typ) → Typ
+  SumN : List (Pair ConstructorName Typ) → Typ
+  Constrained : VarName → Typ → Constraint → Typ 
+
+{-# COMPILE AGDA2HS TypConst #-}
+{-# COMPILE AGDA2HS OpOne #-}
+{-# COMPILE AGDA2HS OpTwo #-}
+{-# COMPILE AGDA2HS Constraint1 #-}
+{-# COMPILE AGDA2HS Constraint #-}
+{-# COMPILE AGDA2HS Typ #-}
+
+{-----------------------------------------------------------------------------
+    Agda - Equality
+------------------------------------------------------------------------------}
+instance
+  iTypConst : Eq TypConst
+  iTypConst ._==_ Bool Bool = True
+  iTypConst ._==_ Bytes Bytes = True
+  iTypConst ._==_ Integer Integer = True
+  iTypConst ._==_ Natural Natural = True
+  iTypConst ._==_ Text Text = True
+  iTypConst ._==_ Rational Rational = True
+  iTypConst ._==_ Unit Unit = True
+  iTypConst ._==_ _ _ = Hs.False
+
+{-# COMPILE AGDA2HS iTypConst derive #-}
+
+-- Created by automati case splitting C^c C^c
+-- and automatic goal finding C^c C^a
+instance
+  iLawfulEqTypConst : IsLawfulEq TypConst
+
+  iLawfulEqTypConst .isEquality Bool Bool = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Bool Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bool Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Bytes = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Bytes Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Bytes Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Integer = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Integer Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Integer Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Natural = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Natural Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Natural Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Text = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Text Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Text Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Rational Rational = Hs.ofY Hs.refl
+  iLawfulEqTypConst .isEquality Rational Unit = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Bool = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Bytes = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Integer = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Natural = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Text = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Rational = Hs.ofN (λ ())
+  iLawfulEqTypConst .isEquality Unit Unit = Hs.ofY Hs.refl
+
+{-----------------------------------------------------------------------------
+    Agda - Syntactic sugar
+------------------------------------------------------------------------------}
+_×_ : Typ → Typ → Typ
+A × B = Two Product2 A B
+
+_+_ : Typ → Typ → Typ
+A + B = Two Sum2 A B