Gabriella439

-- Example Annah programs and their reductions
-- I'll start with simple non-recursive data types so that you can get a feel for the syntax and then work up to recursive data
-- types followed by mutually recursive types

-- Example #1: Bool, the type
$ annah
type Bool
data True
data False
in Bool

Gabriella439

import Numeric.AD

assert = print

eval = id

main = do
    let a x = 2 * x^2 + 3
    let b = eval a 1
    assert (b == 5)         -- Prints `True`

Gabriella439

module Main where

import Data.Array ((..), reverse)
import Data.Int (toNumber)
import Flare (UI, radioGroup)
import Flare.Drawing (runFlareDrawing)
import Graphics.Drawing
import Graphics.Drawing.Font (font, sansSerif, bold)
import Math (cos, sin, pi)
import Prelude

Gabriella439

import Numeric.Natural (Natural)

import qualified Data.Semigroup

-- | @fibonacci n@ computes the @nth@ fibonacci number efficiently using infinite
-- precision integer arithmetic
-- 
-- Try @fibonacci 1000000@
fibonacci :: Natural -> Natural
fibonacci n = x01 (Data.Semigroup.mtimesDefault n m)

Gabriella439

    let Version = ∀(Version : Type) → ∀(v : Text → Version) → Version

in  let VersionRange =
            ∀(VersionRange : Type)
          → ∀(anyVersion : VersionRange)
          → ∀(noVersion : VersionRange)
          → ∀(thisVersion : Version → VersionRange)
          → ∀(notThisVersion : Version → VersionRange)
          → ∀(laterVersion : Version → VersionRange)
          → ∀(earlierVersion : Version → VersionRange)

Gabriella439

let Prelude =
      https://prelude.dhall-lang.org/package.dhall
        sha256:534e4a9e687ba74bfac71b30fc27aa269c0465087ef79bf483e876781602a454

let repeat =
        λ(t : Text)
      → λ(n : Natural)
      → Prelude.`Text`.concat (Prelude.`List`.replicate n Text t)

let spaces = repeat " "

Gabriella439

{- If I remember correctly, one consequence of Gödel's second incompleteness
   theorem is that extensional equivalence is not decidable in general for
   any programming language that can encode Peano numerals.

   The exact case that a programming language fails on may differ from language
   to language (depending on how many tricks they add to try to detect
   non-trivial equivalences).  However, many of them will typically fail to
   detect the equivalence between two ways to encode `increment` for Peano
   numerals.

Gabriella439

-- Credit to: https://news.ycombinator.com/item?id=15186988

let iterate
    : (Natural → Natural) → Natural → Natural
    =   λ(f : Natural → Natural)
      → λ(n : Natural)
      → Natural/fold (n + 1) Natural f 1

let increment : Natural → Natural = λ(n : Natural) → n + 1

Gabriella439

{- This is a bit ugly and inefficient.  See this thread for a discussion about
   adding a `Natural/subtract` built-in to improve this:

   https://github.com/dhall-lang/dhall-lang/issues/602#issuecomment-505484434
-}
let Natural/predecessor : Natural → Natural
        = λ(n : Natural)
        → let result = Natural/fold
          n
          (Optional Natural)

Gabriella439

let Prelude = https://prelude.dhall-lang.org/package.dhall

let FN = Natural/even

let a = 2

let b = 3

let c = 5