HaskellX code examples!

01-DependentTypes.idr

module DependentTypes

TypeOf : {t : Type} -> t -> Type
TypeOf {t} _ = t

-- EXAMPLES

eg0 : TypeOf 3 = Integer
eg0 = Refl

eg1 : TypeOf "hello" = String
eg1 = Refl

eg2 : TypeOf () = ()
eg2 = Refl

----------

the : (t : Type) -> t -> t
the _ x = x

02-LeanTypes.idr

module LeanTypes

-- IDRIS 2

typeof : {t : Type} -> t -> String
typeof {t} _ with (t)
  typeof _ | String = "string"
  typeof _ | Int    = "number"
  typeof _ | Double = "number"
  typeof _ | Bool   = "boolean"
  typeof _ | _      = "object"

-- EXAMPLES

eg0 : typeof "hello" = "string"
eg0 = Refl

eg1 : typeof True = "boolean"
eg1 = Refl

03-Truth.idr

module Truth where

interface      Boolish x       where toBool : x -> Bool
implementation Boolish ()      where toBool _ = False
implementation Boolish Bool    where toBool   = id
implementation Boolish Integer where toBool   = (/=  0)
implementation Boolish Nat     where toBool   = (/=  0)
implementation Boolish String  where toBool   = (/= "")

(&&) : Boolish a => (x : a) -> (y : b) -> if toBool x then b else a
(&&) x y with (toBool x)
  (&&) x y | True  = y
  (&&) x y | False = x

-- EXAMPLES

eg0 : "hello" && 3 = 3
eg0 = Refl

eg1 : "" && True = ""
eg1 = Refl

04-Apply.idr

module Apply where

Applied : Vect k Type -> Type -> Type
Applied [       ] o = o
Applied (i :: is) o = i -> Applied is o

apply : Applied inputs output -> HVect inputs -> output
apply f [       ] = f
apply f (x :: xs) = apply (f x) xs

-- EXAMPLE

add : Nat -> Nat -> Nat
add = (+)

-- These are a bit temperamental, so you might want to run them straight in a shell.
-- For example:
--
-- > apply(add)([2,3])
-- 5 : Integer

eg0 : apply(add)([2,3]) = 5
eg0 = Refl

eg1 : apply(add)([2])(4) = 6
eg1 = Refl

05-Cond.idr

module Cond

data Conditions : Type -> List Type -> Type where
  Nil  : Conditions input []
  (::) : Boolish b
      => HVect [a -> b, a -> c]
      -> Conditions a cs -> Conditions a (c :: cs)

Result : (a -> b) -> Type
Result {b} _ = b

Cond : Conditions a cs -> a -> Type
Cond  [    ]        _ = ()
Cond ([f, g] :: cs) x = if toBool (f x) then Result g else Cond cs x

cond : (c : Conditions a cs) -> (x : a) -> Cond c x
cond  [    ]        _ = ()
cond ([f, g] :: cs) a with (toBool (f a))
  cond ([f, g] :: cs) a | True  = g a
  cond ([f, g] :: cs) a | False = cond cs a

gt2 : Nat -> Bool
gt2 = (> 2)

gt0 : Nat -> Bool
gt0 = (> 0)

always : a -> b -> a
always = const

-- EXAMPLES

eg0 : Nat
eg0 = cond([[gt2, id], [gt0, always("hello")]])(3)

eg1 : String
eg1 = cond([[gt2, id], [gt0, always("hello")]])(2)

06-Converge.idr

module Converge

data FList : Type -> Vect k Type -> Type where
  Nil  : FList i []
  (::) : (i -> o) -> FList i os -> FList i (o :: os)

converge : Applied os o -> FList i os -> i -> o
converge f [       ] = \_ => f
converge f (g :: gs) = \x => converge (f (g x)) gs x

-- EXAMPLES

length : List Double -> Double
length = cast . Prelude.List.length

sum : List Double -> Double
sum = Prelude.Foldable.sum

eg0 : Double
eg0 = converge (/) [sum, length] [1, 2, 3, 4, 5, 6, 7]

concat : String -> String -> String
concat = Prelude.Strings.(++)

eg1 : String
eg1 = converge(concat)([toUpper, toLower])("Yodel")

07-Curry.hs

{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}
module Curry where

import Data.Kind (Type)
import Prelude hiding (curry)

class Compose f g h | f g -> h where
  compose :: f -> g -> h

instance (k ~ (a -> h), Compose f g h) => Compose f (a -> g) k where
  compose f g a = compose f (g a)

instance {-# InCoHeReNt #-} (a ~ c, b ~ d) => Compose (a -> b) c d where
  compose = ($)

type family Curried (args :: Type) (output :: Type) = (f :: Type) where
  Curried (    ) (a -> b) = Curried a b
  Curried (    )  o       = o
  Curried (a, b)  o       = a -> Curried b o
  Curried  i     (a -> b) = i -> Curried a b
  Curried  i      o       = i -> o

class Curry (shape :: Type) (output :: Type) where
  curry :: Curried shape output -> shape -> output

instance Curry a b => Curry () (a -> b) where
  curry f _ = curry f

instance {-# OVERLAPPABLE #-} Curried () o ~ o => Curry () o where
  curry f _ = f

instance Curry b output => Curry (a, b) output where
  curry f (a, b) = curry (f a) b

instance {-# OVERLAPPABLE #-}
    ( Curry a b
    , Curried i (a -> b) ~ (i -> Curried a b)
    )
    => Curry i (a -> b) where
  curry f x = curry (f x)

instance {-# OVERLAPPABLE #-} Curried i o ~ (i -> o)
    => Curry i o where
  curry = id

-- EXAMPLES

g :: Int -> Int -> Int
g = (+)

a :: Int
a = 1

b :: Int
b = 2

eg0, eg1, eg2, eg3 :: Int
eg0 = curry(g)(a)(b)
eg1 = curry(g)(a, b)
eg2 = curry(g)(a)()(b)
eg3 = curry(g)()()()(a)()(b)