jroesch

# Licensed to the Apache Software Foundation (ASF) under one
# or more contributor license agreements.  See the NOTICE file
# distributed with this work for additional information
# regarding copyright ownership.  The ASF licenses this file
# to you under the Apache License, Version 2.0 (the
# "License"); you may not use this file except in compliance
# with the License.  You may obtain a copy of the License at
#
#   http://www.apache.org/licenses/LICENSE-2.0
#

jroesch

using (x : Type, P : x -> Type)
    data HList : (P : x -> Type) -> List x -> Type where
        Nil : HList P []
        (::) : {head : x} -> {tail : List x} -> P head -> HList P tail -> HList P (head :: tail)

head : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> P h
head (h :: _) = h

tail : {h : ty} -> {t : List ty} -> {P : ty -> Type} -> HList P (h :: t) -> HList P t
tail (_ :: t) = t

jroesch

module TypedLogic

import Data.SortedMap

data LType : Type where
  FreshType : LType
  Atom : String -> LType
  DisjUnion : LType -> LType -> LType
  Relation : (Vect n LType) -> LType

jroesch

/* http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt
Generalized Algebraic Datatypes in Scala */

trait Term[A]
case class Lit(x: Int) extends Term[Int]
case class Succ(x: Term[Int]) extends Term[Int]
case class IsZero(x: Term[Int]) extends Term[Boolean]
case class If[A](guard: Term[Boolean], t: Term[A], y: Term[A]) extends Term[A]
case class Pair[A, B](x: Term[A], y: Term[B]) extends Term[(A,B)]
      

jroesch

Given a Haskell Typeclass:

class Point a where 
     distance :: a -> a -> Double

data Point2D = Point2D { x :: Int
                       , y :: Int } deriving (Show, Eq)

instance Point Point2D where
 distance (Point2D x y) (Point2D x' y') = 

jroesch

-- imagine pseudo terms like this
-- def id : Pi (A : Type), A -> A := ...

-- irrelevant.fun 
irrelevant.fun A Type (fun x, x)

-- irrelevant.fun A Type (fun x, x) => fun x, x

-- application of id
(irrelevant.app (fun x, x) A) 10

jroesch

definition position := nat

inductive result (I : Type) : Type -> Type
| fail : Π {R}, I -> list string -> string -> result R
| partial : Π {R}, (I -> result R) -> result R
| done : Π {R}, I -> R -> result R

open result

definition result.map {A B I : Type} (f : A → B) : result I A -> result I B

jroesch

-- module 
structure Map :=
  (M : Type -> Type)
  (K : Type)
  (V : Type)
  (read : K -> V)
  (insert : K -> V -> M K V -> M K V)
  
-- where refinement
definition int_map := { map | map.M = nat }

jroesch

Keybase proof

I hereby claim:

• I am jroesch on github.
• I am jroesch (https://keybase.io/jroesch) on keybase.
• I have a public key ASBf8b_8AaIUVF36T9XaBWbFXAx5x4EKks0ER_dErpVcWwo

To claim this, I am signing this object:

jroesch

import system.IO
import system.ffi
-- import config

-- This is all just config
set_option native.library_path "/Users/jroesch/Git/lean/build/debug"
set_option native.include_path "/Users/jroesch/Git/lean/src"
-- This flag controls whether lean will automatically invoke C++
-- set_option native.compile false
set_option native.emit_dwarf true