Haskell caveats

October 18, 2022 — sameer

‎

1. retrofitting haskell
- 1.1. inconsistent typesystem , you can't return the truth
2. upside
3. building things

1. retrofitting haskell

haskell proofs are partial, if a term corresponding to a type compiles , either term is a valid proof or its eval ll diverge

1.1. inconsistent typesystem , you can't return the truth

bogus :: ((a -> b) -> b) -> Either a b
  -- set b ~ Void

proof : double negation of the law of the excluded middle as applied to a specific proposition

nnlem :: forall a. (Either a (a -> Void) -> Void) -> Void
nnlem f = not_not_a not_a
    where
      not_a :: a -> Void
      not_a = f . Left

      not_not_a :: (a -> Void) -> Void
      not_not_a = f . Right

lem :: Either a (a -> Void)
lem = double_neg_elim nnlem

lem clearly cannot exist because a can encode the proposition that any Turing machine configuration I happen to pick will halt.

bogus :: forall a b. ((a -> b) -> b) -> Either a b
bogus f = case lem @a of
  Left a -> Left a
  Right na -> Right $ f (absurd . na)

so lem is sufficient

via sof

boxing to keep functions pure , async message passing

ml- functor :: ghc- interface

ghc can access unlifted type- hie api, ghc-debug/ event-manager

reify left ghc undecidable termination

encoding y-combinator via infinite newtypes

liquid haskell - ghc elaboration is coherent by default

2. upside

2.1. llvm

2.2. ghc is written in haskell

2.3. construct your own types

3. building things

3.1. ourobros

-- power series , followed by convolution,composition
  p^q+q =zipwith (+) p q

3.2. cloudhaskell

serverStep :: config -> state -> message -> (State,[Message])
  while queue is not empty:
  (new_state, new_msgs) = serverStep
  configs[msg.dst]states[msg.dst]
  msg
  states[msg.dst] = new_state
  put new_msgs into queue

3.3. create your own operators

3.3.1. precedence

prec		non	r
9	!!		.
8			**,^,^^
7	mod, rem,quote
6	+,-
5			:,++
4		`/,<,<`,>,>=
		elem, nonelem
3			&&
2
1	>>,>>=
0			$,$!,seq

Associativity	fix	post	in	pre
left: iff its apps in expression can be grouped l->r			infixl 5 @@
right: r->l			infixr 8 @@
full: l,r
non : not(l,r)			infix 2 @@

Any operator can be made into a normal prefix function by putting parens around it. x + y = (+) x y

Any function can be made into an infix operator by putting backquotes around it. mod x y = x `mod` y.

3.4. Questions

What should passing a list to head :: [a] -> a , return in Haskell?

None if empty, nondeterministically some element of the list otherwise. – @codydroux

When can you safely assume function extensionality, besides simplical sets, topos, sheaves ?

axiom of choice in #typetheory does not have the extensionality properties that the axiom of choice in constructive #settheory does twitter

Author: System administrator

Created: 2022-11-16 Wed 11:35

Validate

Comments? Tweet

Notes