lukaszlew

{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}

data Unit = U

class C (k :: Unit) where
  get :: Int

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

jship

#!/usr/bin/env stack
-- stack --resolver lts-10.8 --install-ghc exec ghci

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

-- A key type for pretend use in looking up a doggo in a database.
newtype Key a = Key { unKey :: String }

mpickering

let
  nixpkgs = import ((import <nixpkgs> { }).fetchFromGitHub {
  owner = "NixOS";
  repo = "nixpkgs";
  rev = "72f07e74f3bcac0635b880fecbd45c17938a6368";
  sha256 = "081qi4hpxzw3w5kphv1qcxyayh542szdshmacz2kpfj9d04d3nzc";
}) { config = { }; };
in
  nixpkgs.callPackage ./pinned-ghc.nix {}

Lysxia

{-# LANGUAGE TypeFamilies, UndecidableInstances #-}

-- https://blog.poisson.chat/posts/2018-07-09-type-gadt.html

module UnMTL where

import Control.Monad.Trans.Reader
import Control.Monad.Trans.State
import Control.Monad.Trans.Except
import Data.Functor.Identity

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

Icelandjack

import Data.Functor.Yoneda
import Data.Char
import Data.Kind

infixr 5
  ·

type  List :: (Type -> Type) -> Constraint
class List f where

i-am-tom

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

wildjcrt

require 'cgi'
require 'active_support'

def verify_and_decrypt_session_cookie(cookie, secret_key_base = Rails.application.secret_key_base)
  config = Rails.application.config
  cookie = CGI::unescape(cookie)
  salt   = config.action_dispatch.authenticated_encrypted_cookie_salt
  encrypted_cookie_cipher = config.action_dispatch.encrypted_cookie_cipher || 'aes-256-gcm'
  # serializer = ActiveSupport::MessageEncryptor::NullSerializer # use this line if you don't know your serializer
  serializer = ActionDispatch::Cookies::JsonSerializer

phadej

{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall #-}