derrickturk

-- https://docs.dhall-lang.org/howtos/How-to-translate-recursive-code-to-Dhall.html

let Person : Type
  = ∀(Person : Type)
  → ∀(MakePerson : { children : List Person, name : Text } → Person)
  → Person

let example : Person
  = λ(Person : Type) →
    λ(MakePerson : { children : List Person, name : Text } → Person) →

derrickturk

-- see https://www.haskellforall.com/2021/01/the-visitor-pattern-is-essentially-same.html
{-# LANGUAGE RankNTypes #-}

-- with ADTs:

data Shape
  = Circle Double Double Double
  | Rectangle Double Double Double Double
  deriving (Eq, Show)

derrickturk

{-# LANGUAGE OverloadedStrings, ViewPatterns, GADTs #-}

import qualified Data.Set as S
import qualified Data.Text as T

data Fucky = Fucky { fuckyNum :: Maybe Double
                   , fuckyString :: Maybe T.Text
                   , fuckyFancyString :: Maybe T.Text
                   , fuckyBoolean :: Maybe Bool
                   } deriving (Eq, Show)

derrickturk

-- https://kata.geosci.ai/challenge/boreholes

import Text.Read (readMaybe)
import Data.Array -- Array sucks, but I want to stay inside the standard library
import Data.List (sort)

{- terrible hack! the problem syntax just happens to look
 - like the innards of a Haskell list.
 -}
parseBoreholes :: String -> Maybe [(Double, Double)]

derrickturk

type poly_fn = { f : 'a. 'a -> 'a }
let ap_poly : poly_fn -> int -> bool -> int * bool = fun pf x y ->
  (pf.f x, pf.f y)

let ap_poly_obj (obj: <f: 'a. 'a -> 'a>) x y = (obj#f x, obj#f y)

let id x = x
let (x, y) = ap_poly { f = id } 3 true
let (x2, y2) = ap_poly_obj (object method f : 'a. 'a -> 'a = id end) 3 true

derrickturk

open System

// types in our system
type Type =
    | IntTy
    | FnTy of Type * Type

// binary operations on integer expressions
type Op =
    | Add

derrickturk

function Counter()
{
    const [count, setCount] = React.useState(0);
    return (
        <div>
            <p>Count = {count}</p>
            <button onClick={() => setCount(count + 1)}>
                Click me! Click me! Do it now, you son of a bitch!
            </button>
        </div>

derrickturk

#lang pie

(claim Vect
  (→ U Nat
    U))
(define Vect
  (λ (A n)
    (iter-Nat
      n
      Trivial

derrickturk

#lang pie

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim repeat

derrickturk

Python 3.6.6 (v3.6.6:4cf1f54eb7, Jun 27 2018, 03:37:03) [MSC v.1900 64 bit (AMD64)] on win32
Type "help", "copyright", "credits" or "license" for more information.
>>> import dis
>>> def f_list():
...     xs = list()
...     for i in range(10):
...         xs.append(i * i)
...     return xs
...
>>> def f_comp():