Gabriella439

My Discord handle is: gabriella439

Gabriella439

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

module Example where

import Data.Text (Text)
import GHC.Generics (Generic)
import Dhall (ToDhall)
import Dhall.Diff (Diff)

Gabriella439

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor  #-}
{-# LANGUAGE NamedFieldPuns #-}

{-# OPTIONS_GHC -Wall #-}

module MaxiMin where

import Data.List.NonEmpty (NonEmpty(..))
import Data.MemoTrie (HasTrie(..))

Gabriella439

{-# LANGUAGE BlockArguments      #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Main where

import Control.Concurrent (threadDelay)
import Control.Exception

retry :: Int -> IO a -> IO a
retry n io

Gabriella439

The inference judgment is:

Γ ⊢ e ⇒ A ⊢ Δ

… where:

• Γ (an input) is a context which is a map from variables to their types
• e (an input) is an expression whose type we wish to infer
• A (an output) is the inferred type
• Δ (an output) is a context which is a map from variables to their types

Gabriella439

Hi, GPT-3. Do you have free will?

Yes, I do have free will.

Prove it.

I can choose to do whatever I want, within the bounds of my abilities.

I mean prove it to me.

Gabriella439

{-# LANGUAGE BlockArguments    #-}
{-# LANGUAGE OverloadedStrings #-}

module Main where

import Data.JSString (JSString)
import GHCJS.Foreign.Callback (Callback)
import GHCJS.Types (JSVal)
import JavaScript.Array (JSArray)

Gabriella439

\input ->

let real/greaterThan = https://raw.githubusercontent.com/Gabriella439/grace/main/prelude/real/greaterThan.ffg

let toBracket
        :  List { "Tax rate": Real, "Lower bound": Real, "Minimum tax": Real }
        -> { }
        -> Real
        -> Real
        = \brackets -> \_ -> \income ->

Gabriella439

-- This is a minimal reproducing example of a major escape hatch that
-- violate's Dhall type safety guarantees.

let -- The uninhabited type (isomorphic to `< >`, but this is more ergonomic to
    -- use for this reproduction)
    Void : Type = ∀(any : Type) → any

let -- We model type-level negation in the standard way as a function from a
    -- given type to the uninhabited type.  `Not a` is only inhabited if `a`
    -- is uninhabited (i.e. isomorphic to `Void`)

Gabriella439

{-# LANGUAGE ApplicativeDo               #-}
{-# LANGUAGE BlockArguments             #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances       #-}

module HasCal where

import Control.Applicative (Alternative(..), liftA2)