natling

# download corpus from https://www.ngrams.info

corpus = open('5-grams non case sensitive.txt')
corpus = [' '.join(line.split()[1:]) for line in corpus]

love = 'i love you'

lines = [line for line in corpus if line.find(love) >= 0]
lines = [line.rjust(len(line) - line.find(love) + max([line.find(love) for line in lines])) for line in lines]
lines = [line.replace(love, ' ' * len(love)) for line in lines]

AndrasKovacs

{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,
             TypeInType, StandaloneDeriving #-}

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake

porglezomp

import Data.Vect

-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max  n     Z    = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max  Z    (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

-- The type here says "the result is" padded to (maximum k n), and is padding plus the original
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)

DaveCTurner

theory Leftpad
  imports Main
begin

definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
  where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"

definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
  where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"

lunaris

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Via where

Icelandjack

-- Response to
--   https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
--   https://twitter.com/sjoerd_visscher/status/975375241932427265

{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}

import Data.Coerce

type f ~> g = forall x. f x -> g x

ekmett

{-# language TypeInType, QuantifiedConstraints, ConstraintKinds, RankNTypes, UndecidableInstances, MultiParamTypeClasses, TypeFamilies, KindSignatures #-}

module QC where

import Data.Constraint
import Data.Functor.Contravariant
import Data.Kind
import Data.Profunctor

type C = (Type -> Type) -> (Type -> Type -> Type) -> Constraint

jmitchell

let List/replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in

let File = Natural in
let Rank = Natural in
let Square = { file : File, rank : Rank } in
let Move = { from : Square, to : Square } in

let Side = < white : {} | black : {} > in
let white = < white = {=} | black : {} > in
let black = < black = {=} | white : {} > in

withoutboats

Notes on adding Constraint Kinds to Rust

Background: Constraint Kinds

a trait can be thought of as a type operator generating a "constraint" - what in Rust would usually be called a bound. For example:

// Declares a new item `Foo` with kind `type -> constraint`
trait Foo { }

sjoerdvisscher

{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
{-# LANGUAGE LambdaCase, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, MultiParamTypeClasses #-}
module Sem where
  
import Data.Algebra
import Data.Constraint
import Data.Constraint.Class1
import Data.Functor.Free

class BaseSem a where