Verity Scheel MonoidMusician

My research ideas

Implement a better typechecker for Dhall. Hopefully still straightforward to implement and with good errors.

I think it will essentially be a reification of the typechecker into data structures such that data still only flows one way, but acts like it flows both ways via substitution. Very tricky.

If I get it implemented, then I can look at performance.

Threads

Nick Scheel
what's the weakest type theory we can define arbitrary finite aleph numbers in? (arbitrary finite beth numbers are easy – just need natural numbers and functions)

Reed Mullanix
Be warned, the cardinals are not very well behaved in constructive math
Pretty much every direction you look, weird stuff starts to happen

Nick Scheel
yeah 🙂
I just find it weird that, with choice, all cardinals are aleph numbers, but beth numbers are the ones that are easy to construct in type theory

Moved to https://github.com/MonoidMusician/senior-project/blob/main/Comprehensive%20Errors.md

	module TestKindMatch where

	import Prelude
	import Data.Maybe (Maybe)

	class Functor1 :: ((Type -> Type) -> Type) -> Constraint
	class Functor1 t where
	map1 :: forall f g. (f ~> g) -> t f -> t g

	data Proxy :: forall k. k -> Type

	module Main where

	import Prelude

	import Effect (Effect)
	import Effect.Aff (Aff)
	import Data.Maybe (Maybe(..))
	import Halogen as H
	import Halogen.Aff as HA
	import Halogen.HTML as HH

	module Main where

	import Prelude

	import Effect (Effect)
	import Effect.Aff (Aff)
	import Data.Maybe (Maybe(..))
	import Halogen as H
	import Halogen.Aff as HA
	import Halogen.HTML as HH

	# Syntax for a metalanguage for writing programming language standards/specifications with an eye towards codegen

	# The data format is very simple: data is either a string or a tuple of data.
	# The idea is that we'll impose some simple types on top of this:
	# Obviously strings, and arrays, possibly associative lists, and then mixed ADTs/enums, which are either plain strings or arrays where the first item is the tag denoting the constructor.
	# I don't have the types figured out yet.

	# Variable names
	variable-name = [_A-Za-z][-_A-Za-z0-9]*
	# A variable can have periods, but they don't mean anything

	{-# LANGUAGE QuantifiedConstraints, MultiParamTypeClasses #-}
	module CoercibleFunctor where

	import Prelude ()

	import Data.Coerce (Coercible, coerce)

	class (forall x y. Coercible x y => Coercible (f x) (f y)) => Functor f where
	map :: forall a b. (a -> b) -> f a -> f b

	module Metalanguage where

	import Prelude

	import Data.Array as Array
	import Data.Maybe (Maybe(..))
	import Data.Traversable (sequence, traverse)

	data Value = ScalarValue String \| VectorValue (Array Value)
	data Sization = NonEmpty \| Any