greatBigDot

{-# LANGUAGE PolyKinds, DataKinds, TypeApplications, TypeOperators, KindSignatures, GADTs, TypeFamilies, ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
-- ^ more extensions might be needed to do what I want to do, idk

-- Defunctionalized higher-order data constructors--are they possible?
module DefunHigherDataCons where

import Data.Kind
import Data.Singletons.TH

greatBigDot

{-# LANGUAGE UnicodeSyntax, NoStarIsType #-}
{-# LANGUAGE GADTs, DataKinds, PolyKinds, PatternSynonyms, ViewPatterns, TypeApplications #-}

module Data.Matrix where

import Data.Kind

-- The usual definitions of Nat and Vec:
data Nat = Z | S Nat

greatBigDot

{-# LANGUAGE UnicodeSyntax, NoStarIsType, LambdaCase #-}
{-# LANGUAGE GADTs, DataKinds, PolyKinds, PatternSynonyms, ViewPatterns, TypeApplications #-}

module Utils where

import Data.Kind

-- The usual definitions of Nat and Vec:
data Nat = Z | S Nat

greatBigDot

{-# LANGUAGE AllowAmbiguousTypes, MultiParamTypeClasses, NoMonomorphismRestriction #-}

module InvalidInference where

class Foo s t where
  foo :: t

-- When commented, GHCi infers this type; when uncommented, it yields a type error:
-- bar :: Foo s t => t
bar = foo

greatBigDot

{-# LANGUAGE LambdaCase, EmptyCase
           , EmptyDataDecls, TypeOperators, LiberalTypeSynonyms,
             ExistentialQuantification, GADTSyntax, GADTs

           , StandaloneDeriving

           , InstanceSigs, FlexibleContexts, MultiParamTypeClasses,
             FlexibleInstances , TypeSynonymInstances , FunctionalDependencies

           , TypeFamilies, TypeFamilyDependencies, DataKinds, PolyKinds,

greatBigDot

-- A constructive proof that there is no biggest natural. I.e., we construct the
-- type "there is no biggest natural" and construct an element of it. The
-- naturals, the order relation on them, etc. are likewise all defined
-- constructively.

module 4SWC where

-- Just to take care of the universe levels; you can safely ignore it:
open import Agda.Primitive

greatBigDot

#!/bin/bash
set +eu

# # Uncomment this to see what a normal array would do:
# array=( "${FUNCNAME[@]}" )
# unset FUNCNAME
# FUNCNAME=( "${array[@]}" )
# unset array

# # Or uncomment this for the same result in a more direct fashion:

greatBigDot

{-# LANGUAGE EmptyDataDecls, TypeOperators, LiberalTypeSynonyms, ExistentialQuantification, ExplicitForAll #-}
{-# LANGUAGE GADTSyntax, GADTs, DuplicateRecordFields, NamedFieldPuns, MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances, FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies, TypeFamilies, TypeFamilyDependencies, ConstraintKinds, ScopedTypeVariables #-}
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures, TypeInType, TypeApplications, ImplicitParams, NamedWildCards, RankNTypes #-}
{-# LANGUAGE ExplicitNamespaces, MonoLocalBinds, DisambiguateRecordFields, ConstrainedClassMethods #-}
--- ^ I just grabbed anything that looked remotely useful.

module Algebraics.Data.Field where

import GHC.TypeLits

greatBigDot

<interactive>:1:6: error:
    Not in scope: ‘System.IO.hSetBuffering’
    No module named ‘System.IO’ is imported.

<interactive>:1:30: error:
    Not in scope: ‘System.IO.stdin’
    No module named ‘System.IO’ is imported.

<interactive>:1:46: error:
    Not in scope: data constructor ‘System.IO.NoBuffering’