bbarker

The type system of Unison is a form of predicative system F, but the intent of this article is not to discuss the type system formally, but to give some understanding for how "extremal types" function within the type system. Extremal types in this sense are types at the bottom or top of some hierarchy, and it should be noted that extremal is not a word used elsewhere in this exact sense, to our knowledge.

Unison Type Hierarchy (lattice of types)

The lattice of types in Unison has top and bottom types:

⊤ = ∃e.e -- Called Any
⊥ = ∀a.a -- Called Void

edmundsmith

Method for Emulating Higher-Kinded Types in Rust

Intro

I've been fiddling about with an idea lately, looking at how higher-kinded types can be represented in such a way that we can reason with them in Rust here and now, without having to wait a couple years for what would be a significant change to the language and compiler.

There have been multiple discussions on introducing higher-ranked polymorphism into Rust, using Haskell-style Higher-Kinded Types (HKTs) or Scala-looking Generalised Associated Types (GATs). The benefit of higher-ranked polymorphism is to allow higher-level, richer abstractions and pattern expression than just the rank-1 polymorphism we have today.

As an example, currently we can express this type:

yougg

set http or socks proxy environment variables

# set http proxy
export http_proxy=http://PROXYHOST:PROXYPORT

# set http proxy with user and password
export http_proxy=http://USERNAME:PASSWORD@PROXYHOST:PROXYPORT

# set http proxy with user and password (with special characters)

tonymorris

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveFunctor #-}

import Control.Lens
import Prelude hiding (readFile, writeFile, print)
import qualified Prelude as Prelude(readFile, writeFile, print)

casperbp

(*** Turing Machines in Coq *)

(** Some preliminary types we'll use *)
CoInductive CoList (A: Type) := CONS (a:A) (t:CoList A) | NIL.

Arguments CONS [A] _ _.
Arguments NIL [A].

CoInductive Delay A := HERE (a:A) | LATER (_:Delay A).
 

tonymorris

• All things are either:

  • A sum, which is a hypothetical/potential (not necessarily corresponding) constructor name, followed by +, followed by one or more things.
  • A product, which is a hypothetical/potential (not necessarily corresponding) field name, followed by *, followed by exactly one thing.

• Left + (7 + (() * ()))

  • Left 7 :: Either Int a
  • This 7 :: These Int a
  • Const 7 :: Const Int a

• name * (Cons + (F + (() * ())) (Cons + (r + (() * ())) (Cons * (e + (() * ())) (Cons + (d + (() * ())) Nil))))

gallais

{-# OPTIONS --copatterns #-}

module UntypedLambda where

open import Size
open import Function

mutual

  data Delay (A : Set) (i : Size) : Set where

alpmestan

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Files where

import Control.Monad.IO.Class
import Control.Monad.Trans.Either

ekmett

##Theorem:

Given fmap id = id:

fmap f . fmap g = fmap (f . g)

To prove this we're going to need a few lemmas:

chrisdone

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology