oisdk

{-# LANGUAGE UnicodeSyntax        #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Kind
import Data.Functor.Const

oisdk

-- Selective lets us do "monadic" binds where the domain is restricted
-- to the countable types (which can be infinite).

{-# LANGUAGE TypeOperators     #-}
{-# LANGUAGE PatternSynonyms   #-}
{-# LANGUAGE ViewPatterns      #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts  #-}

import GHC.Generics

oisdk

{-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators  #-}

import Data.Kind
import Data.Coerce

data Nat = Z | S Nat

data Vec (a :: Type) (n :: Nat) where
  Nil :: Vec a Z
  (:-) :: a -> Vec a n -> Vec a (S n)

oisdk

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveFoldable, DeriveTraversable, DeriveFunctor #-}

import Data.List (mapAccumL)

data Stream a = a :< Stream a deriving (Functor, Foldable, Traversable)
infixr 5 :<

instance Show a => Show (Stream a) where
  showsPrec n = showsPrec n . foldr (:) []

oisdk

import Test.QuickCheck
import Data.Tree.Binary.Preorder (Tree(..), drawTree)
import Control.Arrow (first)
import Data.List (unfoldr)

fromList :: [a] -> Tree a
fromList xs = head (l (foldr f b xs 1 2))
  where
    b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
    

oisdk

{-# LANGUAGE DeriveFunctor, LambdaCase, BlockArguments, BangPatterns, RankNTypes, GeneralisedNewtypeDeriving, OverloadedLists, TypeFamilies #-}

{-# OPTIONS_GHC -Wall #-}

import Control.Monad
import Control.Applicative
import Numeric.Natural
import GHC.Exts
import GHC.Base (build)

oisdk

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-}

{-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-}

import Data.Monoid (Sum(..))
import Data.Kind (Type)

data Nat = Z | S Nat

data Fin (n :: Nat) where

oisdk

{-# OPTIONS --cubical --safe #-}

module Curry where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open import Cubical.Data.Nat

oisdk

data ω : Type₀ where
  zero : ω
  suc : ω → ω
  inf : ω
  suc-inf : suc inf ≡ inf

ω′ : Type₀
ω′ = Maybe ℕ

zero′ : ω′

oisdk

init :: [a] -> [a]
init xs = foldr f b xs Nothing
  where
    b Nothing = error "init: empty list"
    b _       = []
    
    f x xs Nothing  = xs (Just x)
    f y xs (Just x) = x : xs (Just y)