Gabriella Gonzalez Gabriella439

My Discord handle is: gabriella439

The inference judgment is:

Γ ⊢ e ⇒ A ⊢ Δ

… where:

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.

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

	module Example where

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

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

	{-# OPTIONS_GHC -Wall #-}

	module MaxiMin where

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

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

	module Main where

	import Control.Concurrent (threadDelay)
	import Control.Exception

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

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

	module Main where

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

	\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 ->

	-- 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`)

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

	module HasCal where

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